<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
"http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">
<html xmlns="http://www.w3.org/1999/xhtml">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
<link href="common/css/sf.css" rel="stylesheet" type="text/css"/>
<title>IndProp: 归纳定义的命题</title>
</head>
<link href="common/jquery-ui/jquery-ui.css" rel="stylesheet">
<script src="common/jquery-ui/external/jquery/jquery.js"></script>
<script src="common/jquery-ui/jquery-ui.js"></script>
<script src="common/toggleproofs.js"></script>
<link href="common/css/lf.css" rel="stylesheet" type="text/css"/>

<body>

<div id="page">

<div id="header">
<a href='https://coq-zh.github.io/SF-zh/index.html'>
<img src='common/media/image/sf_logo_sm.png'></a>
</br><a href='index.html'>  <span class='booktitleinheader'>Volume 1: 逻辑基础</span><br></br>
<ul id='menu'>
   <a href='toc.html'><li class='section_name'>目录</li></a>
   <a href='coqindex.html'><li class='section_name'>索引</li></a>
   <a href='deps.html'><li class='section_name'>路线</li></a>
</ul>
</a></div>

<div id="main">

<h1 class="libtitle">IndProp<span class="subtitle">归纳定义的命题</span></h1>


<div class="code code-tight">

<span class="id" type="keyword">Set</span> <span class="id" type="var">Warnings</span> "-notation-overridden,-parsing".<br/>
<span class="id" type="var">From</span> <span class="id" type="var">LF</span> <span class="id" type="keyword">Require</span> <span class="id" type="keyword">Export</span> <span class="id" type="var">Logic</span>.<br/>
<span class="id" type="keyword">Require</span> <span class="id" type="var">Coq.omega.Omega</span>.<br/>
</div>

<div class="doc">
<a name="lab206"></a><h1 class="section">归纳定义的命题</h1>

<div class="paragraph"> </div>

 在 <a href="Logic.html"><span class="inlineref">Logic</span></a> 一章中，我们学习了多种方式来书写命题，包括合取、析取和存在量词。
    在本章中，我们引入另一种新的方式：<b>归纳定义（Inductive Definitions）</b>。 
<div class="paragraph"> </div>

 在前面的章节中，我们已经见过两种表述 <span class="inlinecode"><span class="id" type="var">n</span></span> 为偶数的方式了：

<div class="paragraph"> </div>

      (1) <span class="inlinecode"><span class="id" type="var">evenb</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span>，以及

<div class="paragraph"> </div>

      (2) <span class="inlinecode"><span style='font-size:120%;'>&exist;</span></span> <span class="inlinecode"><span class="id" type="var">k</span>,</span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">k</span></span>。

<div class="paragraph"> </div>

    然而还有一种方式是通过如下规则来建立 <span class="inlinecode"><span class="id" type="var">n</span></span> 的偶数性质：

<div class="paragraph"> </div>

<ul class="doclist">
<li> 规则 <span class="inlinecode"><span class="id" type="var">ev_0</span></span>: <span class="inlinecode">0</span> 是偶数。

</li>
<li> 规则 <span class="inlinecode"><span class="id" type="var">ev_SS</span></span>: 如果 <span class="inlinecode"><span class="id" type="var">n</span></span> 是偶数, 那么 <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span> 也是偶数。 
</li>
</ul>

<div class="paragraph"> </div>

 为了理解这个新的偶数性质定义如何工作，我们可想象如何证明 <span class="inlinecode">4</span> 是偶数。
    根据规则 <span class="inlinecode"><span class="id" type="var">ev_SS</span></span>，需要证明 <span class="inlinecode">2</span> 是偶数。这时，只要证明 <span class="inlinecode">0</span> 是偶数，
    我们可继续通过规则 <span class="inlinecode"><span class="id" type="var">ev_SS</span></span> 确保它成立。而使用规则 <span class="inlinecode"><span class="id" type="var">ev_0</span></span> 可直接证明 <span class="inlinecode">0</span> 是偶数。
<div class="paragraph"> </div>

 接下来的课程中，我们会看到很多类似方式定义的命题。
    在非形式化的讨论中，使用轻量化的记法有助于阅读和书写。
    <b>推断规则（Inference Rules）</b>是其中的一种： 
<div class="paragraph"> </div>

<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (ev_0) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">even&nbsp;0</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">even&nbsp;n</td>
  <td class="infrulenamecol" rowspan="3">
    (ev_SS) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">even&nbsp;(S&nbsp;(S&nbsp;n))</td>
  <td></td>
</td>
</table></center>
<div class="paragraph"> </div>


<div class="paragraph"> </div>

    若将前文所述的规则重新排版成推断规则，我们可以这样阅读它，如果线上方的
    <b>前提（premises）</b>成立，那么线下方的<b>结论（conclusion）</b>成立。
    比如，规则 <span class="inlinecode"><span class="id" type="var">ev_SS</span></span> 读做如果 <span class="inlinecode"><span class="id" type="var">n</span></span> 满足 <span class="inlinecode"><span class="id" type="var">even</span></span>，那么 <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span> 也满足。
    如果一条规则在线上方没有前提，则结论直接成立。

<div class="paragraph"> </div>

    我们可以通过组合推断规则来展示证明。下面展示如何转译 <span class="inlinecode">4</span> 是偶数的证明： 
<div class="paragraph"> </div>


<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;--------&nbsp;&nbsp;(<span class="id" type="var">ev_0</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">even</span>&nbsp;0<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;--------&nbsp;(<span class="id" type="var">ev_SS</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">even</span>&nbsp;2<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;--------&nbsp;(<span class="id" type="var">ev_SS</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">even</span>&nbsp;4
<div class="paragraph"> </div>

</div>

<div class="paragraph"> </div>


<div class="paragraph"> </div>

    （为什么我们把这样的证明称之为“树”（而非其他，比如“栈”）？
    因为一般来说推断规则可以有多个前提。我们很快就会看到一些例子。 
<div class="paragraph"> </div>

<a name="lab207"></a><h2 class="section">偶数性的归纳定义</h2>
 基于上述，可将偶数性质的定义翻译为在 Coq 中使用 <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> 声明的定义，
    声明中每一个构造子对应一个推断规则： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">even</span> : <span class="id" type="var">nat</span> → <span class="id" type="keyword">Prop</span> :=<br/>
| <span class="id" type="var">ev_0</span> : <span class="id" type="var">even</span> 0<br/>
| <span class="id" type="var">ev_SS</span> (<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>) (<span class="id" type="var">H</span> : <span class="id" type="var">even</span> <span class="id" type="var">n</span>) : <span class="id" type="var">even</span> (<span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>)).<br/>
</div>

<div class="doc">
这个定义同之前其他 <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> 的使用有一个重要的区别：
    我们所定义的并不是一个 <span class="inlinecode"><span class="id" type="keyword">Type</span></span>，而是一个将 <span class="inlinecode"><span class="id" type="var">nat</span></span> 映射到 <span class="inlinecode"><span class="id" type="keyword">Prop</span></span> 的函数——即关于数的性质。
    我们曾见过结果也是函数的归纳定义，比如 <span class="inlinecode"><span class="id" type="var">list</span></span>，其类型是 <span class="inlinecode"><span class="id" type="keyword">Type</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="keyword">Type</span></span> 。
    真正要关注的是，由于 <span class="inlinecode"><span class="id" type="var">even</span></span> 中出现在冒号<b>右侧</b>的 <span class="inlinecode"><span class="id" type="var">nat</span></span> 参数是 <b>未命名</b> 的，
    这允许在不同的构造子类型中使用不同的值：例如 <span class="inlinecode"><span class="id" type="var">ev_0</span></span> 类型中的 <span class="inlinecode">0</span> 以及 <span class="inlinecode"><span class="id" type="var">ev_SS</span></span>
    类型中的 <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span>。

<div class="paragraph"> </div>

    相反，<span class="inlinecode"><span class="id" type="var">list</span></span> 的定义以<b>全局方式</b>命名了冒号<b>左侧</b>的参数 <span class="inlinecode"><span class="id" type="var">X</span></span>，
    强迫 <span class="inlinecode"><span class="id" type="var">nil</span></span> 和 <span class="inlinecode"><span class="id" type="var">cons</span></span> 的结果为同一个类型（<span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span>）。
    如果在定义 <span class="inlinecode"><span class="id" type="var">even</span></span> 时我们将 <span class="inlinecode"><span class="id" type="var">nat</span></span> 置于冒号左侧，会得到如下错误： 
</div>
<div class="code code-tight">

<span class="id" type="var">Fail</span> <span class="id" type="keyword">Inductive</span> <span class="id" type="var">wrong_ev</span> (<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>) : <span class="id" type="keyword">Prop</span> :=<br/>
| <span class="id" type="var">wrong_ev_0</span> : <span class="id" type="var">wrong_ev</span> 0<br/>
| <span class="id" type="var">wrong_ev_SS</span> : <span class="id" type="var">wrong_ev</span> <span class="id" type="var">n</span> → <span class="id" type="var">wrong_ev</span> (<span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>)).<br/>
<span class="comment">(*&nbsp;===&gt;&nbsp;Error:&nbsp;Last&nbsp;occurrence&nbsp;of&nbsp;"<span class="inlinecode"><span class="id" type="var">wrong_ev</span></span>"&nbsp;must&nbsp;have&nbsp;"<span class="inlinecode"><span class="id" type="var">n</span></span>"<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;as&nbsp;1st&nbsp;argument&nbsp;in&nbsp;"<span class="inlinecode"><span class="id" type="var">wrong_ev</span></span> <span class="inlinecode">0</span>".&nbsp;*)</span><br/>
</div>

<div class="doc">
在 <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> 定义中，类型构造子的冒号左侧的参数叫做形参（Parameter），
    而右侧的叫做索引（Index）。

<div class="paragraph"> </div>

    例如，在 <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode">(<span class="id" type="var">X</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="keyword">Type</span>)</span> <span class="inlinecode">:=</span> <span class="inlinecode">...</span> 中，<span class="inlinecode"><span class="id" type="var">X</span></span> 是一个形参；而在
    <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">nat</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="keyword">Prop</span></span> <span class="inlinecode">:=</span> <span class="inlinecode">...</span> 中，未命名的 <span class="inlinecode"><span class="id" type="var">nat</span></span> 参数是一个索引。 
<div class="paragraph"> </div>

 在 Coq 中，我们可以认为 <span class="inlinecode"><span class="id" type="var">even</span></span> 定义了一个性质 <span class="inlinecode"><span class="id" type="var">ev</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">nat</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="keyword">Prop</span></span>，其包括原语定理
    <span class="inlinecode"><span class="id" type="var">ev_0</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode">0</span> 和 <span class="inlinecode"><span class="id" type="var">ev_SS</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span> <span class="inlinecode"><span class="id" type="var">n</span>,</span> <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">→</span> <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>))</span>。 
<div class="paragraph"> </div>

 该定义也可写作如下形式...

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;<span class="id" type="keyword">Inductive</span>&nbsp;<span class="id" type="var">even</span>&nbsp;:&nbsp;<span class="id" type="var">nat</span>&nbsp;→&nbsp;<span class="id" type="keyword">Prop</span>&nbsp;:=<br/>
&nbsp;&nbsp;|&nbsp;<span class="id" type="var">ev_0</span>&nbsp;:&nbsp;<span class="id" type="var">even</span>&nbsp;0<br/>
&nbsp;&nbsp;|&nbsp;<span class="id" type="var">ev_SS</span>&nbsp;:&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>,&nbsp;<span class="id" type="var">even</span>&nbsp;<span class="id" type="var">n</span>&nbsp;→&nbsp;<span class="id" type="var">even</span>&nbsp;(<span class="id" type="var">S</span>&nbsp;(<span class="id" type="var">S</span>&nbsp;<span class="id" type="var">n</span>)).
<div class="paragraph"> </div>

</div>

<div class="paragraph"> </div>

 ... 以便让 <span class="inlinecode"><span class="id" type="var">ev_SS</span></span> 的类型更加直白。 
<div class="paragraph"> </div>

 这些 “定理构造子” 等同于已经证明过的定理。
    具体来说，我们可以使用 Coq 中的 <span class="inlinecode"><span class="id" type="tactic">apply</span></span> 策略和规则名称来证明某个数的 <span class="inlinecode"><span class="id" type="var">even</span></span> 性质…… 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ev_4</span> : <span class="id" type="var">even</span> 4.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">ev_SS</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">ev_SS</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">ev_0</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
……或使用函数应用的语法： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ev_4'</span> : <span class="id" type="var">even</span> 4.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">apply</span> (<span class="id" type="var">ev_SS</span> 2 (<span class="id" type="var">ev_SS</span> 0 <span class="id" type="var">ev_0</span>)). <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
我们同样可以对前提中使用到 <span class="inlinecode"><span class="id" type="var">even</span></span> 的定理进行证明。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ev_plus4</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>, <span class="id" type="var">even</span> <span class="id" type="var">n</span> → <span class="id" type="var">even</span> (4 + <span class="id" type="var">n</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span>. <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">Hn</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">ev_SS</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">ev_SS</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">Hn</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
更一般地，我们可以证明以任意数乘 2 是偶数： 
<div class="paragraph"> </div>

<a name="lab208"></a><h4 class="section">练习：1 星, standard (ev_double)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ev_double</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">even</span> (<span class="id" type="var">double</span> <span class="id" type="var">n</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab209"></a><h1 class="section">在证明中使用证据</h1>

<div class="paragraph"> </div>

 除了<b>构造</b>证据（evidence）来表示某个数是偶数，我们还可以对这些证据进行<b>推理</b>。

<div class="paragraph"> </div>

    对 <span class="inlinecode"><span class="id" type="var">even</span></span> 而言，使用 <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> 声明来引入 <span class="inlinecode"><span class="id" type="var">even</span></span> 不仅仅表示在 Coq
    中 <span class="inlinecode"><span class="id" type="var">ev_0</span></span> 和 <span class="inlinecode"><span class="id" type="var">ev_SS</span></span> 这样的构造子是合法的方式来构造偶数证明的证据，
    他们也是<b>仅有的</b>方式。 
<div class="paragraph"> </div>

 换句话说，如果某人展示了对于 <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> 的证据 <span class="inlinecode"><span class="id" type="var">E</span></span>，那么我们知道 <span class="inlinecode"><span class="id" type="var">E</span></span>
    必是二者其一：

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">E</span></span> 是 <span class="inlinecode"><span class="id" type="var">ev_0</span></span>（且 <span class="inlinecode"><span class="id" type="var">n</span></span> 为 <span class="inlinecode"><span class="id" type="var">O</span></span>）, 或

</li>
<li> <span class="inlinecode"><span class="id" type="var">E</span></span> 是 <span class="inlinecode"><span class="id" type="var">ev_SS</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span> <span class="inlinecode"><span class="id" type="var">E'</span></span>（且 <span class="inlinecode"><span class="id" type="var">n</span></span> 为 <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span>)</span>, <span class="inlinecode"><span class="id" type="var">E'</span></span> 为
        <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span> 的证据）. 
</li>
</ul>

<div class="paragraph"> </div>

 这样的形式暗示着，我们可以像分析归纳定义的数据结构一样分析形如 <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span>
    的假设；特别地，对于这类证据使用<b>归纳（induction）</b>和<b>分类讨论（case
    analysis）</b>来进行论证也是可行的。让我们通过一些例子来学习实践中如何使用他们。 
<div class="paragraph"> </div>

<a name="lab210"></a><h2 class="section">对证据进行反演</h2>

<div class="paragraph"> </div>

 Suppose we are proving some fact involving a number <span class="inlinecode"><span class="id" type="var">n</span></span>, and
    we are given <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> as a hypothesis.  We already know how to
    perform case analysis on <span class="inlinecode"><span class="id" type="var">n</span></span> using <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> or <span class="inlinecode"><span class="id" type="tactic">induction</span></span>,
    generating separate subgoals for the case where <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">O</span></span> and the
    case where <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span> for some <span class="inlinecode"><span class="id" type="var">n'</span></span>.  But for some proofs we may
    instead want to analyze the evidence that <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> _directly_. As
    a tool, we can prove our characterization of evidence for
    <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span>, using <span class="inlinecode"><span class="id" type="tactic">destruct</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ev_inversion</span> :<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>), <span class="id" type="var">even</span> <span class="id" type="var">n</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">n</span> = 0) ∨ (<span style='font-size:120%;'>&exist;</span><span class="id" type="var">n'</span>, <span class="id" type="var">n</span> = <span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">n'</span>) ∧ <span class="id" type="var">even</span> <span class="id" type="var">n'</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">E</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">E</span> <span class="id" type="keyword">as</span> [ | <span class="id" type="var">n'</span> <span class="id" type="var">E'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E&nbsp;=&nbsp;ev_0&nbsp;:&nbsp;even&nbsp;0&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">left</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E&nbsp;=&nbsp;ev_SS&nbsp;n'&nbsp;E'&nbsp;:&nbsp;even&nbsp;(S&nbsp;(S&nbsp;n'))&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">right</span>. <span style='font-size:120%;'>&exist;</span><span class="id" type="var">n'</span>. <span class="id" type="tactic">split</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">E'</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
用 <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> 解构证据即可证明下述定理： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ev_minus2</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">even</span> <span class="id" type="var">n</span> → <span class="id" type="var">even</span> (<span class="id" type="var">pred</span> (<span class="id" type="var">pred</span> <span class="id" type="var">n</span>)).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">E</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">E</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">n'</span> <span class="id" type="var">E'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E&nbsp;=&nbsp;ev_0&nbsp;*)</span> <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">ev_0</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E&nbsp;=&nbsp;ev_SS&nbsp;n'&nbsp;E'&nbsp;*)</span> <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">E'</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
However, this variation cannot easily be handled with <span class="inlinecode"><span class="id" type="tactic">destruct</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">evSS_ev</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">even</span> (<span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>)) → <span class="id" type="var">even</span> <span class="id" type="var">n</span>.<br/>
</div>

<div class="doc">
直观来说，我们知道支撑前提的证据不会由 <span class="inlinecode"><span class="id" type="var">ev_0</span></span> 组成，因为 <span class="inlinecode">0</span> 和 <span class="inlinecode"><span class="id" type="var">S</span></span> 是
    <span class="inlinecode"><span class="id" type="var">nat</span></span> 类型不同的构造子；由此 <span class="inlinecode"><span class="id" type="var">ev_SS</span></span> 是唯一需要应对的情况（译注：<span class="inlinecode"><span class="id" type="var">ev_0</span></span> 无条件成立）。
    不幸的是，<span class="inlinecode"><span class="id" type="tactic">destruct</span></span> 并没有如此智能，它仍然为我们生成两个子目标。
    更坏的是，于此同时最终目标没有改变，也无法为完成证明提供任何有用的信息。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">E</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">E</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">n'</span> <span class="id" type="var">E'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E&nbsp;=&nbsp;ev_0.&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="comment">(*&nbsp;我们须证明&nbsp;<span class="inlinecode"><span class="id" type="var">n</span></span>&nbsp;是偶数，但没有任何有用的假设信息可以使用！&nbsp;*)</span><br/>
<span class="id" type="keyword">Abort</span>.<br/>
</div>

<div class="doc">
究竟发生了什么？应用 <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> 把性质的参数替换为对应于构造子的值。
    这对于证明 <span class="inlinecode"><span class="id" type="var">ev_minus2'</span></span> 是有帮助的，因为在最终目标中直接使用到了参数 <span class="inlinecode"><span class="id" type="var">n</span></span>。
    然而，这对于 <span class="inlinecode"><span class="id" type="var">evSS_ev</span></span> 并没有帮助，因为被替换掉的 <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span> 并没有在其他地方被使用。
<div class="paragraph"> </div>

 We could patch this proof by replacing the goal <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span>,
    which does not mention the replaced term <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>)</span>, by the
    equivalent goal <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode">(<span class="id" type="var">pred</span></span> <span class="inlinecode">(<span class="id" type="var">pred</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n</span>))))</span>, which does mention
    this term, after which <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> can make progress. But it is
    more straightforward to use our inversion lemma. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">evSS_ev</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>, <span class="id" type="var">even</span> (<span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>)) → <span class="id" type="var">even</span> <span class="id" type="var">n</span>.<br/>
<span class="id" type="keyword">Proof</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">ev_inversion</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">H</span>.<br/>
&nbsp;- <span class="id" type="tactic">discriminate</span> <span class="id" type="var">H</span>.<br/>
&nbsp;- <span class="id" type="tactic">destruct</span> <span class="id" type="var">H</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">n'</span> [<span class="id" type="var">Hnm</span> <span class="id" type="var">Hev</span>]]. <span class="id" type="tactic">injection</span> <span class="id" type="var">Hnm</span>.<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intro</span> <span class="id" type="var">Heq</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">Heq</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">Hev</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Coq provides a tactic called <span class="inlinecode"><span class="id" type="tactic">inversion</span></span>, which does the work of
    our inversion lemma and more besides. 
<div class="paragraph"> </div>

 The <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> tactic can detect (1) that the first case
    (<span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode">0</span>) does not apply and (2) that the <span class="inlinecode"><span class="id" type="var">n'</span></span> that appears in the
    <span class="inlinecode"><span class="id" type="var">ev_SS</span></span> case must be the same as <span class="inlinecode"><span class="id" type="var">n</span></span>.  It has an "<span class="inlinecode"><span class="id" type="keyword">as</span></span>" variant
    similar to <span class="inlinecode"><span class="id" type="tactic">destruct</span></span>, allowing us to assign names rather than
    have Coq choose them. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">evSS_ev'</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">even</span> (<span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>)) → <span class="id" type="var">even</span> <span class="id" type="var">n</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">E</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">E</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">n'</span> <span class="id" type="var">E'</span>].<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;We&nbsp;are&nbsp;in&nbsp;the&nbsp;<span class="inlinecode"><span class="id" type="var">E</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">ev_SS</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span> <span class="inlinecode"><span class="id" type="var">E'</span></span>&nbsp;case&nbsp;now.&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">E'</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
The <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> tactic can apply the principle of explosion to
    "obviously contradictory" hypotheses involving inductive
    properties, something that takes a bit more work using our
    inversion lemma. For example: 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">one_not_even</span> : ¬<span class="id" type="var">even</span> 1.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">ev_inversion</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">H</span> <span class="id" type="keyword">as</span> [ | [<span class="id" type="var">m</span> [<span class="id" type="var">Hm</span> <span class="id" type="var">_</span>]]].<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">discriminate</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">discriminate</span> <span class="id" type="var">Hm</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">one_not_even'</span> : ¬<span class="id" type="var">even</span> 1.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab211"></a><h4 class="section">练习：1 星, standard (inversion_practice)</h4>
 利用 <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> 策略证明以下结论。如想进一步练习，请使用反演定理证明之。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">SSSSev__even</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">even</span> (<span class="id" type="var">S</span> (<span class="id" type="var">S</span> (<span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>)))) → <span class="id" type="var">even</span> <span class="id" type="var">n</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab212"></a><h4 class="section">练习：1 星, standard (even5_nonsense)</h4>
 请使用 <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> 策略证明以下结果。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">even5_nonsense</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">even</span> 5 → 2 + 2 = 9.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 The <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> tactic does quite a bit of work. When
    applied to equalities, as a special case, it does the work of both
    <span class="inlinecode"><span class="id" type="tactic">discriminate</span></span> and <span class="inlinecode"><span class="id" type="tactic">injection</span></span>. In addition, it carries out the
    <span class="inlinecode"><span class="id" type="tactic">intros</span></span> and <span class="inlinecode"><span class="id" type="tactic">rewrite</span></span>s that are typically necessary in the case
    of <span class="inlinecode"><span class="id" type="tactic">injection</span></span>. It can also be applied, more generally, to analyze
    evidence for inductively defined propositions.  As examples, we'll
    use it to reprove some theorems from <span class="inlinecode"><span class="id" type="var">Tactics.v</span></span>. 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">inversion_ex<sub>1</sub></span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">o</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;[<span class="id" type="var">n</span>; <span class="id" type="var">m</span>] = [<span class="id" type="var">o</span>; <span class="id" type="var">o</span>] →<br/>
&nbsp;&nbsp;[<span class="id" type="var">n</span>] = [<span class="id" type="var">m</span>].<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">o</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">reflexivity</span>. <span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">inversion_ex<sub>2</sub></span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">S</span> <span class="id" type="var">n</span> = <span class="id" type="var">O</span> →<br/>
&nbsp;&nbsp;2 + 2 = 5.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">contra</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">contra</span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<span class="inlinecode"><span class="id" type="tactic">inversion</span></span> 的工作原理大致如下：假设 <span class="inlinecode"><span class="id" type="var">H</span></span> 指代上下文中的假设 <span class="inlinecode"><span class="id" type="var">P</span></span>，
    且 <span class="inlinecode"><span class="id" type="var">P</span></span> 由 <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> 归纳定义，则对于 <span class="inlinecode"><span class="id" type="var">P</span></span> 每一种可能的构造，<span class="inlinecode"><span class="id" type="tactic">inversion</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span>
    各为其生成子目标。子目标中自相矛盾者被忽略，证明其余子命题即可得证原命题。
    在证明子目标时，上下文中的 <span class="inlinecode"><span class="id" type="var">H</span></span> 会替换为 <span class="inlinecode"><span class="id" type="var">P</span></span> 的构造条件，
    即其构造子所需参数以及必要的等式关系。例如：倘若 <span class="inlinecode"><span class="id" type="var">ev</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> 由 <span class="inlinecode"><span class="id" type="var">evSS</span></span> 构造，
    上下文中会引入参数 <span class="inlinecode"><span class="id" type="var">n'</span></span>、<span class="inlinecode"><span class="id" type="var">ev</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span>，以及等式 <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">n</span></span>。 
<div class="paragraph"> </div>

 上面的 <span class="inlinecode"><span class="id" type="var">ev_double</span></span> 练习展示了偶数性质的一种新记法，其被之前的两种记法所蕴含。
    （因为，由  <a href="Logic.html"><span class="inlineref">Logic</span></a> 一章中的 <span class="inlinecode"><span class="id" type="var">even_bool_prop</span></span>，我们已经知道
    他们是互相等价的。）
    为了展示这三种方式的一致性，我们需要下面的引理： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">ev_even_firsttry</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">even</span> <span class="id" type="var">n</span> → <span style='font-size:120%;'>&exist;</span><span class="id" type="var">k</span>, <span class="id" type="var">n</span> = <span class="id" type="var">double</span> <span class="id" type="var">k</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;课上已完成&nbsp;*)</span><br/>
</div>

<div class="doc">
我们可以尝试使用分类讨论或对 <span class="inlinecode"><span class="id" type="var">n</span></span> 进行归纳。
    但由于 <span class="inlinecode"><span class="id" type="var">even</span></span> 在前提中出现，如同之前章节的一些例子，这种策略或许无法行得通。
    如此我们似乎可以首先尝试对 <span class="inlinecode"><span class="id" type="var">even</span></span> 的证据进行反演。
    确实，第一个分类可以被平凡地证明。 
</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">E</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">E</span> <span class="id" type="keyword">as</span> [| <span class="id" type="var">n'</span> <span class="id" type="var">E'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E&nbsp;=&nbsp;ev_0&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span>0. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E&nbsp;=&nbsp;ev_SS&nbsp;n'&nbsp;E'&nbsp;*)</span> <span class="id" type="tactic">simpl</span>.<br/>
</div>

<div class="doc">
不幸地是，第二个分类要困难一些。我们需要证明 <span class="inlinecode"><span style='font-size:120%;'>&exist;</span></span> <span class="inlinecode"><span class="id" type="var">k</span>,</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">double</span></span> <span class="inlinecode"><span class="id" type="var">k</span></span>，
    但唯一可用的假设是 <span class="inlinecode"><span class="id" type="var">E'</span></span>，也即 <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span> 成立。但这对证明并没有帮助，
    我们似乎被卡住了，而对 <span class="inlinecode"><span class="id" type="var">E</span></span> 进行分类讨论是徒劳的。

<div class="paragraph"> </div>

    如果仔细观察第二个（子）目标，我们可以发现一些有意思的事情：
    对 <span class="inlinecode"><span class="id" type="var">E</span></span> 进行分类讨论，我们可以把要证明的原始目标归约到另一个上，
    其涉及到另一个 <span class="inlinecode"><span class="id" type="var">even</span></span> 的证据： <span class="inlinecode"><span class="id" type="var">E'</span></span>。
    形式化地说，我们可以通过展示如下证据来完成证明：

<div class="paragraph"> </div>


<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">k'</span>,&nbsp;<span class="id" type="var">n'</span>&nbsp;=&nbsp;<span class="id" type="var">double</span>&nbsp;<span class="id" type="var">k'</span>,
<div class="paragraph"> </div>

</div>

<div class="paragraph"> </div>

    这同原始的命题是等价的，只是 <span class="inlinecode"><span class="id" type="var">n'</span></span> 被替换为 n。确实，通过这个中间结果完成证明
    并不困难。  
</div>
<div class="code code-tight">

&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">assert</span> (<span class="id" type="var">I</span> : (<span style='font-size:120%;'>&exist;</span><span class="id" type="var">k'</span>, <span class="id" type="var">n'</span> = <span class="id" type="var">double</span> <span class="id" type="var">k'</span>) →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&exist;</span><span class="id" type="var">k</span>, <span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">n'</span>) = <span class="id" type="var">double</span> <span class="id" type="var">k</span>)).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;{ <span class="id" type="tactic">intros</span> [<span class="id" type="var">k'</span> <span class="id" type="var">Hk'</span>]. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hk'</span>. <span style='font-size:120%;'>&exist;</span>(<span class="id" type="var">S</span> <span class="id" type="var">k'</span>). <span class="id" type="tactic">reflexivity</span>. }<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">I</span>. <span class="comment">(*&nbsp;将原始目标归约到新目标上&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Abort</span>.<br/>
</div>

<div class="doc">
<a name="lab213"></a><h2 class="section">对证据进行归纳</h2>

<div class="paragraph"> </div>

 在 <a href="Induction.html"><span class="inlineref">Induction</span></a> 一章中，我们曾尝试使用分类讨论来证明其实需要使用归纳才能证明的命题。
    上面的情形看起来似曾相识，但并不是巧合。这一次，解决方法仍然是使用……归纳！

<div class="paragraph"> </div>

    对证据和对数据使用 <span class="inlinecode"><span class="id" type="tactic">induction</span></span> 具有同样的行为：它导致 Coq 对每个可用于构造证据的
    构造子生成一个子目标，同时对递归出现的问题性质提供了归纳假设。

<div class="paragraph"> </div>

    To prove a property of <span class="inlinecode"><span class="id" type="var">n</span></span> holds for all numbers for which <span class="inlinecode"><span class="id" type="var">even</span></span>
    <span class="inlinecode"><span class="id" type="var">n</span></span> holds, we can use induction on <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span>. This requires us to
    prove two things, corresponding to the two ways in which <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span>
    could have been constructed. If it was constructed by <span class="inlinecode"><span class="id" type="var">ev_0</span></span>, then
    <span class="inlinecode"><span class="id" type="var">n</span>=0</span>, and the property must hold of <span class="inlinecode">0</span>. If it was constructed by
    <span class="inlinecode"><span class="id" type="var">ev_SS</span></span>, then the evidence of <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n</span></span> is of the form <span class="inlinecode"><span class="id" type="var">ev_SS</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span>
    <span class="inlinecode"><span class="id" type="var">E'</span></span>, where <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode">(<span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span>)</span> and <span class="inlinecode"><span class="id" type="var">E'</span></span> is evidence for <span class="inlinecode"><span class="id" type="var">even</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span>. In
    this case, the inductive hypothesis says that the property we are
    trying to prove holds for <span class="inlinecode"><span class="id" type="var">n'</span></span>. 
<div class="paragraph"> </div>

 让我们再次尝试证明这个引理： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">ev_even</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">even</span> <span class="id" type="var">n</span> → <span style='font-size:120%;'>&exist;</span><span class="id" type="var">k</span>, <span class="id" type="var">n</span> = <span class="id" type="var">double</span> <span class="id" type="var">k</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">E</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">E</span> <span class="id" type="keyword">as</span> [|<span class="id" type="var">n'</span> <span class="id" type="var">E'</span> <span class="id" type="var">IH</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E&nbsp;=&nbsp;ev_0&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span>0. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;E&nbsp;=&nbsp;ev_SS&nbsp;n'&nbsp;E'<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;同时&nbsp;IH&nbsp;:&nbsp;exists&nbsp;k',&nbsp;n'&nbsp;=&nbsp;double&nbsp;k'&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">IH</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">k'</span> <span class="id" type="var">Hk'</span>].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hk'</span>. <span style='font-size:120%;'>&exist;</span>(<span class="id" type="var">S</span> <span class="id" type="var">k'</span>). <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
这里我们看到 Coq 对 <span class="inlinecode"><span class="id" type="var">E'</span></span> 产生了 <span class="inlinecode"><span class="id" type="var">IH</span></span>，而 <span class="inlinecode"><span class="id" type="var">E'</span></span> 是唯一递归出现的
    <span class="inlinecode"><span class="id" type="var">even</span></span> 命题。 由于 <span class="inlinecode"><span class="id" type="var">E'</span></span> 中涉及到 <span class="inlinecode"><span class="id" type="var">n'</span></span>，这个归纳假设是关于 <span class="inlinecode"><span class="id" type="var">n'</span></span> 的，
    而非关于 <span class="inlinecode"><span class="id" type="var">n</span></span> 或其他数字的。  
<div class="paragraph"> </div>

 关于偶数性质的第二个和第三个定义的等价关系如下： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ev_even_iff</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">even</span> <span class="id" type="var">n</span> ↔ <span style='font-size:120%;'>&exist;</span><span class="id" type="var">k</span>, <span class="id" type="var">n</span> = <span class="id" type="var">double</span> <span class="id" type="var">k</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span>. <span class="id" type="tactic">split</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;<span class="nowrap"><span style='font-size:85%;'><span style='vertical-align:5%;'><span style='letter-spacing:-.2em;'>-</span></span>&gt;</span></span>&nbsp;*)</span> <span class="id" type="tactic">apply</span> <span class="id" type="var">ev_even</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;&lt;-&nbsp;*)</span> <span class="id" type="tactic">intros</span> [<span class="id" type="var">k</span> <span class="id" type="var">Hk</span>]. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">Hk</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">ev_double</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
我们会在后面的章节中看到，对证据进行归纳在很多领域里是一种常用的技术，
    特别是在形式化程序语言的语义时，由于其中很多有趣的性质都是归纳定义的。 
<div class="paragraph"> </div>

 下面的练习提供了一些简单的例子，来帮助你熟悉这项技术。 
<div class="paragraph"> </div>

<a name="lab214"></a><h4 class="section">练习：2 星, standard (ev_sum)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ev_sum</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>, <span class="id" type="var">even</span> <span class="id" type="var">n</span> → <span class="id" type="var">even</span> <span class="id" type="var">m</span> → <span class="id" type="var">even</span> (<span class="id" type="var">n</span> + <span class="id" type="var">m</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab215"></a><h4 class="section">练习：4 星, advanced, optional (even</b>ev)</h4>
 一般来说，有很多种方式来归纳地定义一个性质。比如说，下面是关于
    <span class="inlinecode"><span class="id" type="var">even</span></span> 的另一种（蹩脚的）定义：
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">even'</span> : <span class="id" type="var">nat</span> → <span class="id" type="keyword">Prop</span> :=<br/>
| <span class="id" type="var">even'_0</span> : <span class="id" type="var">even'</span> 0<br/>
| <span class="id" type="var">even'_2</span> : <span class="id" type="var">even'</span> 2<br/>
| <span class="id" type="var">even'_sum</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span> (<span class="id" type="var">Hn</span> : <span class="id" type="var">even'</span> <span class="id" type="var">n</span>) (<span class="id" type="var">Hm</span> : <span class="id" type="var">even'</span> <span class="id" type="var">m</span>) : <span class="id" type="var">even'</span> (<span class="id" type="var">n</span> + <span class="id" type="var">m</span>).<br/>
</div>

<div class="doc">
请证明这个定义在逻辑上等同于前述定义。（当进入到归纳步骤时，你可能会想参考一下上一个定理。）
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">even'_ev</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>, <span class="id" type="var">even'</span> <span class="id" type="var">n</span> ↔ <span class="id" type="var">even</span> <span class="id" type="var">n</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab216"></a><h4 class="section">练习：3 星, advanced, recommended (ev_ev__ev)</h4>
 在本题中找到适合进行归纳的项需要一点技巧： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ev_ev__ev</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">even</span> (<span class="id" type="var">n</span>+<span class="id" type="var">m</span>) → <span class="id" type="var">even</span> <span class="id" type="var">n</span> → <span class="id" type="var">even</span> <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab217"></a><h4 class="section">练习：3 星, standard, optional (ev_plus_plus)</h4>
 这个练习仅仅需要使用前述引理，而不需要使用归纳或分类讨论，尽管一些重写可能会比较乏味。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">ev_plus_plus</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">p</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">even</span> (<span class="id" type="var">n</span>+<span class="id" type="var">m</span>) → <span class="id" type="var">even</span> (<span class="id" type="var">n</span>+<span class="id" type="var">p</span>) → <span class="id" type="var">even</span> (<span class="id" type="var">m</span>+<span class="id" type="var">p</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab218"></a><h1 class="section">归纳关系</h1>

<div class="paragraph"> </div>

 我们可以认为被一个数所参数化的命题（比如 <span class="inlinecode"><span class="id" type="var">even</span></span>）是一个<b>性质</b>，也即，
    它定义了 <span class="inlinecode"><span class="id" type="var">nat</span></span>　的一个子集，其中的数可以被证明满足此命题。
    以同样的方式，我们可认为有两个参数的命题是一个<b>关系</b>，也即，它定义了一个
    可满足此命题的序对集合。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">Playground</span>.<br/>
</div>

<div class="doc">
一个很有用的例子是整数的“小于等于”关系。
<div class="paragraph"> </div>

 下面的定义应当是比较直观的。它提供了两种方法来描述一个数小于等于另一个数的证据：
    要么可观察到两个数相等，或提供证据显示第一个数小于等于第二个数的前继。　
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">le</span> : <span class="id" type="var">nat</span> → <span class="id" type="var">nat</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">le_n</span> <span class="id" type="var">n</span> : <span class="id" type="var">le</span> <span class="id" type="var">n</span> <span class="id" type="var">n</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">le_S</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span> (<span class="id" type="var">H</span> : <span class="id" type="var">le</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span>) : <span class="id" type="var">le</span> <span class="id" type="var">n</span> (<span class="id" type="var">S</span> <span class="id" type="var">m</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Notation</span> "m ≤ n" := (<span class="id" type="var">le</span> <span class="id" type="var">m</span> <span class="id" type="var">n</span>).<br/>
</div>

<div class="doc">
类似于证明 <span class="inlinecode"><span class="id" type="var">even</span></span> 这样的性质，使用 <span class="inlinecode"><span class="id" type="var">le_n</span></span> 和 <span class="inlinecode"><span class="id" type="var">le_S</span></span> 构造子来证明关于 <span class="inlinecode">≤</span>
    的事实遵循了同样的模式。我们可以对构造子使用 <span class="inlinecode"><span class="id" type="tactic">apply</span></span> 策略来证明 <span class="inlinecode">≤</span> 目标
    （比如证明 <span class="inlinecode">3≤3</span> 或 <span class="inlinecode">3≤6</span>），也可以使用 <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> 策略来从上下文中 <span class="inlinecode">≤</span>
    的假设里抽取信息（比如证明 <span class="inlinecode">(2≤1)</span> <span class="inlinecode">→</span> <span class="inlinecode">2+2=5</span>）。 
<div class="paragraph"> </div>

 这里提供一些完备性检查。（请注意，尽管这同我们在开始课程时编写的
    函数“单元测试”类似，但我们在这里必须明确地写下他们的证明——<span class="inlinecode"><span class="id" type="tactic">simpl</span></span> 和
    <span class="inlinecode"><span class="id" type="tactic">reflexivity</span></span> 并不会有效果，因为这些证明不仅仅是对表达式进行简化。）  
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">test_le<sub>1</sub></span> :<br/>
&nbsp;&nbsp;3 ≤ 3.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;课上已完成&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">le_n</span>. <span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">test_le<sub>2</sub></span> :<br/>
&nbsp;&nbsp;3 ≤ 6.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;课上已完成&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">le_S</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">le_S</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">le_S</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">le_n</span>. <span class="id" type="keyword">Qed</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">test_le<sub>3</sub></span> :<br/>
&nbsp;&nbsp;(2 ≤ 1) → 2 + 2 = 5.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;课上已完成&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>2</sub></span>. <span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
现在“严格小于”关系 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">&lt;</span> <span class="inlinecode"><span class="id" type="var">m</span></span> 可以使用 <span class="inlinecode"><span class="id" type="var">le</span></span> 来定义。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">End</span> <span class="id" type="var">Playground</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">lt</span> (<span class="id" type="var">n</span> <span class="id" type="var">m</span>:<span class="id" type="var">nat</span>) := <span class="id" type="var">le</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>) <span class="id" type="var">m</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Notation</span> "m &lt; n" := (<span class="id" type="var">lt</span> <span class="id" type="var">m</span> <span class="id" type="var">n</span>).<br/>
</div>

<div class="doc">
这里展示了一些定义于自然数上的关系：
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">square_of</span> : <span class="id" type="var">nat</span> → <span class="id" type="var">nat</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">sq</span> <span class="id" type="var">n</span> : <span class="id" type="var">square_of</span> <span class="id" type="var">n</span> (<span class="id" type="var">n</span> * <span class="id" type="var">n</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">next_nat</span> : <span class="id" type="var">nat</span> → <span class="id" type="var">nat</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">nn</span> <span class="id" type="var">n</span> : <span class="id" type="var">next_nat</span> <span class="id" type="var">n</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>).<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Inductive</span> <span class="id" type="var">next_even</span> : <span class="id" type="var">nat</span> → <span class="id" type="var">nat</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">ne_1</span> <span class="id" type="var">n</span> : <span class="id" type="var">even</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>) → <span class="id" type="var">next_even</span> <span class="id" type="var">n</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">ne_2</span> <span class="id" type="var">n</span> (<span class="id" type="var">H</span> : <span class="id" type="var">even</span> (<span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>))) : <span class="id" type="var">next_even</span> <span class="id" type="var">n</span> (<span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>)).<br/>
</div>

<div class="doc">
<a name="lab219"></a><h4 class="section">练习：2 星, standard, optional (total_relation)</h4>
 请定一个二元归纳关系 <span class="inlinecode"><span class="id" type="var">total_relation</span></span> 对每一个自然数的序对成立。 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab220"></a><h4 class="section">练习：2 星, standard, optional (empty_relation)</h4>
 请定一个二元归纳关系 <span class="inlinecode"><span class="id" type="var">empty_relation</span></span> 对自然数永远为假。 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 From the definition of <span class="inlinecode"><span class="id" type="var">le</span></span>, we can sketch the behaviors of
    <span class="inlinecode"><span class="id" type="tactic">destruct</span></span>, <span class="inlinecode"><span class="id" type="tactic">inversion</span></span>, and <span class="inlinecode"><span class="id" type="tactic">induction</span></span> on a hypothesis <span class="inlinecode"><span class="id" type="var">H</span></span>
    providing evidence of the form <span class="inlinecode"><span class="id" type="var">le</span></span> <span class="inlinecode"><span class="id" type="var">e<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">e<sub>2</sub></span></span>.  Doing <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span>
    will generate two cases. In the first case, <span class="inlinecode"><span class="id" type="var">e<sub>1</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">e<sub>2</sub></span></span>, and it
    will replace instances of <span class="inlinecode"><span class="id" type="var">e<sub>2</sub></span></span> with <span class="inlinecode"><span class="id" type="var">e<sub>1</sub></span></span> in the goal and context.
    In the second case, <span class="inlinecode"><span class="id" type="var">e<sub>2</sub></span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span> for some <span class="inlinecode"><span class="id" type="var">n'</span></span> for which <span class="inlinecode"><span class="id" type="var">le</span></span> <span class="inlinecode"><span class="id" type="var">e<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span>
    holds, and it will replace instances of <span class="inlinecode"><span class="id" type="var">e<sub>2</sub></span></span> with <span class="inlinecode"><span class="id" type="var">S</span></span> <span class="inlinecode"><span class="id" type="var">n'</span></span>.
    Doing <span class="inlinecode"><span class="id" type="tactic">inversion</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span> will remove impossible cases and add generated
    equalities to the context for further use. Doing <span class="inlinecode"><span class="id" type="tactic">induction</span></span> <span class="inlinecode"><span class="id" type="var">H</span></span>
    will, in the second case, add the induction hypothesis that the
    goal holds when <span class="inlinecode"><span class="id" type="var">e<sub>2</sub></span></span> is replaced with <span class="inlinecode"><span class="id" type="var">n'</span></span>. 
<div class="paragraph"> </div>

<a name="lab221"></a><h4 class="section">练习：3 星, standard, optional (le_exercises)</h4>
 这里展示一些 <span class="inlinecode">≤</span> 和 <span class="inlinecode">&lt;</span> 关系的事实，我们在接下来的课程中将会用到他们。
    证明他们将会是非常有益的练习。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">le_trans</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span>, <span class="id" type="var">m</span> ≤ <span class="id" type="var">n</span> → <span class="id" type="var">n</span> ≤ <span class="id" type="var">o</span> → <span class="id" type="var">m</span> ≤ <span class="id" type="var">o</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">O_le_n</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>,<br/>
&nbsp;&nbsp;0 ≤ <span class="id" type="var">n</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">n_le_m__Sn_le_Sm</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> ≤ <span class="id" type="var">m</span> → <span class="id" type="var">S</span> <span class="id" type="var">n</span> ≤ <span class="id" type="var">S</span> <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">Sn_le_Sm__n_le_m</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">S</span> <span class="id" type="var">n</span> ≤ <span class="id" type="var">S</span> <span class="id" type="var">m</span> → <span class="id" type="var">n</span> ≤ <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">le_plus_l</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">a</span> <span class="id" type="var">b</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">a</span> ≤ <span class="id" type="var">a</span> + <span class="id" type="var">b</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">plus_lt</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n<sub>1</sub></span> <span class="id" type="var">n<sub>2</sub></span> <span class="id" type="var">m</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">n<sub>1</sub></span> + <span class="id" type="var">n<sub>2</sub></span> &lt; <span class="id" type="var">m</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">n<sub>1</sub></span> &lt; <span class="id" type="var">m</span> ∧ <span class="id" type="var">n<sub>2</sub></span> &lt; <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">lt</span>.<br/>
&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">lt_S</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> &lt; <span class="id" type="var">m</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> &lt; <span class="id" type="var">S</span> <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">leb_complete</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> &lt;=? <span class="id" type="var">m</span> = <span class="id" type="var">true</span> → <span class="id" type="var">n</span> ≤ <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
提示：在下面的问题中，对 <span class="inlinecode"><span class="id" type="var">m</span></span> 进行归纳会使证明容易一些。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">leb_correct</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> ≤ <span class="id" type="var">m</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> &lt;=? <span class="id" type="var">m</span> = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
提示：这个定理可以不通过使用 <span class="inlinecode"><span class="id" type="tactic">induction</span></span> 来证明。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">leb_true_trans</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">o</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> &lt;=? <span class="id" type="var">m</span> = <span class="id" type="var">true</span> → <span class="id" type="var">m</span> &lt;=? <span class="id" type="var">o</span> = <span class="id" type="var">true</span> → <span class="id" type="var">n</span> &lt;=? <span class="id" type="var">o</span> = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab222"></a><h4 class="section">练习：2 星, standard, optional (leb_iff)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">leb_iff</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">n</span> &lt;=? <span class="id" type="var">m</span> = <span class="id" type="var">true</span> ↔ <span class="id" type="var">n</span> ≤ <span class="id" type="var">m</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">R</span>.<br/>
</div>

<div class="doc">
<a name="lab223"></a><h4 class="section">练习：3 星, standard, recommended (R_provability)</h4>
 通过同样的方式，我们可以定义三元关系、四元关系等。例如，考虑以下定义在自然数上的三元关系： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">R</span> : <span class="id" type="var">nat</span> → <span class="id" type="var">nat</span> → <span class="id" type="var">nat</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;&nbsp;| <span class="id" type="var">c<sub>1</sub></span> : <span class="id" type="var">R</span> 0 0 0<br/>
&nbsp;&nbsp;&nbsp;| <span class="id" type="var">c<sub>2</sub></span> <span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span> (<span class="id" type="var">H</span> : <span class="id" type="var">R</span> <span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span>) : <span class="id" type="var">R</span> (<span class="id" type="var">S</span> <span class="id" type="var">m</span>) <span class="id" type="var">n</span> (<span class="id" type="var">S</span> <span class="id" type="var">o</span>)<br/>
&nbsp;&nbsp;&nbsp;| <span class="id" type="var">c<sub>3</sub></span> <span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span> (<span class="id" type="var">H</span> : <span class="id" type="var">R</span> <span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span>) : <span class="id" type="var">R</span> <span class="id" type="var">m</span> (<span class="id" type="var">S</span> <span class="id" type="var">n</span>) (<span class="id" type="var">S</span> <span class="id" type="var">o</span>)<br/>
&nbsp;&nbsp;&nbsp;| <span class="id" type="var">c<sub>4</sub></span> <span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span> (<span class="id" type="var">H</span> : <span class="id" type="var">R</span> (<span class="id" type="var">S</span> <span class="id" type="var">m</span>) (<span class="id" type="var">S</span> <span class="id" type="var">n</span>) (<span class="id" type="var">S</span> (<span class="id" type="var">S</span> <span class="id" type="var">o</span>))) : <span class="id" type="var">R</span> <span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span><br/>
&nbsp;&nbsp;&nbsp;| <span class="id" type="var">c<sub>5</sub></span> <span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span> (<span class="id" type="var">H</span> : <span class="id" type="var">R</span> <span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span>) : <span class="id" type="var">R</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">o</span>.<br/>
</div>

<div class="doc">

<div class="paragraph"> </div>

<ul class="doclist">
<li> 下列哪个命题是可以被证明的？
<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">R</span></span> <span class="inlinecode">1</span> <span class="inlinecode">1</span> <span class="inlinecode">2</span>

</li>
<li> <span class="inlinecode"><span class="id" type="var">R</span></span> <span class="inlinecode">2</span> <span class="inlinecode">2</span> <span class="inlinecode">6</span>

<div class="paragraph"> </div>


<div class="paragraph"> </div>


</li>
</ul>

</li>
<li> 如果在 <span class="inlinecode"><span class="id" type="var">R</span></span> 的定义中我们丢弃 <span class="inlinecode"><span class="id" type="var">c<sub>5</sub></span></span> 构造子，可被证明的集合会发生变化吗？
      简要（一句话）解释你的答案。

<div class="paragraph"> </div>


</li>
<li> 如果在 <span class="inlinecode"><span class="id" type="var">R</span></span> 的定义中我们丢弃 <span class="inlinecode"><span class="id" type="var">c<sub>4</sub></span></span> 构造子，可被证明的集合会发生变化吗？
      简要（一句话）解释你的答案。

</li>
</ul>

<div class="paragraph"> </div>

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_R_provability</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab224"></a><h4 class="section">练习：3 星, standard, optional (R_fact)</h4>
 关系 <span class="inlinecode"><span class="id" type="var">R</span></span> 其实编码了一个熟悉的函数。请找出这个函数，定义它并在 Coq 中证明他们等价。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">fR</span> : <span class="id" type="var">nat</span> → <span class="id" type="var">nat</span> → <span class="id" type="var">nat</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">R_equiv_fR</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span>, <span class="id" type="var">R</span> <span class="id" type="var">m</span> <span class="id" type="var">n</span> <span class="id" type="var">o</span> ↔ <span class="id" type="var">fR</span> <span class="id" type="var">m</span> <span class="id" type="var">n</span> = <span class="id" type="var">o</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="code code-tight">

<span class="id" type="keyword">End</span> <span class="id" type="var">R</span>.<br/>
</div>

<div class="doc">
<a name="lab225"></a><h4 class="section">练习：2 星, advanced (subsequence)</h4>
 如果一个列表的所有元素以相同的顺序出现在另一个列表之中（但允许其中出现其他额外的元素），
    我们把第一个列表称作第二个列表的<b>子序列</b>。 例如：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[1;2;3]
<div class="paragraph"> </div>

</div>
    是以下所有列表的子序列

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[1;2;3]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[1;1;1;2;2;3]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[1;2;7;3]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[5;6;1;9;9;2;7;3;8]
<div class="paragraph"> </div>

</div>
    但<b>不是</b>以下列表的子序列

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[1;2]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[1;3]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;[5;6;2;1;7;3;8].
<div class="paragraph"> </div>

</div>

<div class="paragraph"> </div>

<ul class="doclist">
<li> 在 <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">nat</span></span> 上定一个归纳命题 <span class="inlinecode"><span class="id" type="var">subseq</span></span>，其表达了子序列的涵义。
      （提示：你需要三个分类。）

<div class="paragraph"> </div>


</li>
<li> 证明子序列的自反关系 <span class="inlinecode"><span class="id" type="var">subseq_refl</span></span>，也即任何列表是它自身的子序列。

<div class="paragraph"> </div>


</li>
<li> 证明关系 <span class="inlinecode"><span class="id" type="var">subseq_app</span></span> 对任意列表 <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span>，<span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">l<sub>3</sub></span></span>，如果 <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> 是 <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span>
      的子序列，那么 <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> 也是 <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span> <span class="inlinecode">++</span> <span class="inlinecode"><span class="id" type="var">l<sub>3</sub></span></span> 的子序列。

<div class="paragraph"> </div>


</li>
<li> （可选的，困难）证明子序列的传递关系 <span class="inlinecode"><span class="id" type="var">subseq_trans</span></span>——也即，如果 <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> 是 <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span>
      的子序列，且 <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span> 是 <span class="inlinecode"><span class="id" type="var">l<sub>3</sub></span></span> 的子序列，那么 <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> 是 <span class="inlinecode"><span class="id" type="var">l<sub>3</sub></span></span> 的子序列。
      （提示：仔细选择进行归纳的项！） 
</li>
</ul>

</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">subseq</span> : <span class="id" type="var">list</span> <span class="id" type="var">nat</span> → <span class="id" type="var">list</span> <span class="id" type="var">nat</span> → <span class="id" type="keyword">Prop</span> :=<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">subseq_refl</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">nat</span>), <span class="id" type="var">subseq</span> <span class="id" type="var">l</span> <span class="id" type="var">l</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">subseq_app</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">l<sub>1</sub></span> <span class="id" type="var">l<sub>2</sub></span> <span class="id" type="var">l<sub>3</sub></span> : <span class="id" type="var">list</span> <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">subseq</span> <span class="id" type="var">l<sub>1</sub></span> <span class="id" type="var">l<sub>2</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">subseq</span> <span class="id" type="var">l<sub>1</sub></span> (<span class="id" type="var">l<sub>2</sub></span> ++ <span class="id" type="var">l<sub>3</sub></span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">subseq_trans</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">l<sub>1</sub></span> <span class="id" type="var">l<sub>2</sub></span> <span class="id" type="var">l<sub>3</sub></span> : <span class="id" type="var">list</span> <span class="id" type="var">nat</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">subseq</span> <span class="id" type="var">l<sub>1</sub></span> <span class="id" type="var">l<sub>2</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">subseq</span> <span class="id" type="var">l<sub>2</sub></span> <span class="id" type="var">l<sub>3</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">subseq</span> <span class="id" type="var">l<sub>1</sub></span> <span class="id" type="var">l<sub>3</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab226"></a><h4 class="section">练习：2 星, standard, optional (R_provability2)</h4>
 假设我们在 Coq 中有如下定义：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">Inductive</span>&nbsp;<span class="id" type="var">R</span>&nbsp;:&nbsp;<span class="id" type="var">nat</span>&nbsp;→&nbsp;<span class="id" type="var">list</span>&nbsp;<span class="id" type="var">nat</span>&nbsp;→&nbsp;<span class="id" type="keyword">Prop</span>&nbsp;:=<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">c<sub>1</sub></span>&nbsp;:&nbsp;<span class="id" type="var">R</span>&nbsp;0&nbsp;[]<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">c<sub>2</sub></span>&nbsp;:&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>&nbsp;<span class="id" type="var">l</span>,&nbsp;<span class="id" type="var">R</span>&nbsp;<span class="id" type="var">n</span>&nbsp;<span class="id" type="var">l</span>&nbsp;→&nbsp;<span class="id" type="var">R</span>&nbsp;(<span class="id" type="var">S</span>&nbsp;<span class="id" type="var">n</span>)&nbsp;(<span class="id" type="var">n</span>&nbsp;::&nbsp;<span class="id" type="var">l</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|&nbsp;<span class="id" type="var">c<sub>3</sub></span>&nbsp;:&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span>&nbsp;<span class="id" type="var">l</span>,&nbsp;<span class="id" type="var">R</span>&nbsp;(<span class="id" type="var">S</span>&nbsp;<span class="id" type="var">n</span>)&nbsp;<span class="id" type="var">l</span>&nbsp;→&nbsp;<span class="id" type="var">R</span>&nbsp;<span class="id" type="var">n</span>&nbsp;<span class="id" type="var">l</span>.
<div class="paragraph"> </div>

</div>
    下列命题哪个是可被证明的？

<div class="paragraph"> </div>

<ul class="doclist">
<li> <span class="inlinecode"><span class="id" type="var">R</span></span> <span class="inlinecode">2</span> <span class="inlinecode">[1;0]</span>

</li>
<li> <span class="inlinecode"><span class="id" type="var">R</span></span> <span class="inlinecode">1</span> <span class="inlinecode">[1;2;1;0]</span>

</li>
<li> <span class="inlinecode"><span class="id" type="var">R</span></span> <span class="inlinecode">6</span> <span class="inlinecode">[3;2;1;0]</span>  
</li>
</ul>

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab227"></a><h1 class="section">案例学习：正则表达式</h1>

<div class="paragraph"> </div>

 性质 <span class="inlinecode"><span class="id" type="var">even</span></span> 提供了一个简单的例子来展示归纳定义和其基础的推理技巧，
    但这还不是什么激动人心的东西——毕竟，<span class="inlinecode"><span class="id" type="var">even</span></span> 等价于我们之前见过的两个非归纳的定义，
    而看起来归纳定义并没有提供什么好处。为了更好地展示归纳定义的表达能力，
    我们继续使用它来建模计算机科学中的一个经典概念——正则表达式。 
<div class="paragraph"> </div>

 正则表达式是用来描述字符串集合的一种简单语言，定义如下： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">reg_exp</span> {<span class="id" type="var">T</span> : <span class="id" type="keyword">Type</span>} : <span class="id" type="keyword">Type</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">EmptySet</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">EmptyStr</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Char</span> (<span class="id" type="var">t</span> : <span class="id" type="var">T</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">App</span> (<span class="id" type="var">r<sub>1</sub></span> <span class="id" type="var">r<sub>2</sub></span> : <span class="id" type="var">reg_exp</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">Union</span> (<span class="id" type="var">r<sub>1</sub></span> <span class="id" type="var">r<sub>2</sub></span> : <span class="id" type="var">reg_exp</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">Star</span> (<span class="id" type="var">r</span> : <span class="id" type="var">reg_exp</span>).<br/>
</div>

<div class="doc">
请注意这个定义是<b>多态的</b>：<span class="inlinecode"><span class="id" type="var">reg_exp</span></span> <span class="inlinecode"><span class="id" type="var">T</span></span> 中的正则表达式描述了字符串，
    而其中的字符取自 <span class="inlinecode"><span class="id" type="var">T</span></span>——也即，<span class="inlinecode"><span class="id" type="var">T</span></span> 的元素构成的列表。

<div class="paragraph"> </div>

    （同一般的实践略有不同，我们不要求类型 <span class="inlinecode"><span class="id" type="var">T</span></span> 是有限的。由此可形成一些不同的正则表达式
    理论，但对于我们在本章的目的而言并无不同。） 
<div class="paragraph"> </div>

 我们通过以下规则来构建正则表达式和字符串，这些规则定义了正则表达式何时匹配一个字符串：

<div class="paragraph"> </div>

<ul class="doclist">
<li> 表达式 <span class="inlinecode"><span class="id" type="var">EmptySet</span></span> 不匹配任何字符串。

<div class="paragraph"> </div>


</li>
<li> 表达式 <span class="inlinecode"><span class="id" type="var">EmptyStr</span></span> 匹配空字符串 <span class="inlinecode">[]</span>.

<div class="paragraph"> </div>


</li>
<li> 表达式 <span class="inlinecode"><span class="id" type="var">Char</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> 匹配单个字符构成的字符串 <span class="inlinecode">[<span class="id" type="var">x</span>]</span>.

<div class="paragraph"> </div>


</li>
<li> 如果 <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span> 匹配 <span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span></span>, 且 <span class="inlinecode"><span class="id" type="var">re<sub>2</sub></span></span> 匹配 <span class="inlinecode"><span class="id" type="var">s<sub>2</sub></span></span>, 那么 <span class="inlinecode"><span class="id" type="var">App</span></span> <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">re<sub>2</sub></span></span> 匹配 <span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span></span> <span class="inlinecode">++</span> <span class="inlinecode"><span class="id" type="var">s<sub>2</sub></span></span>.

<div class="paragraph"> </div>


</li>
<li> 如果 <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">re<sub>2</sub></span></span> 中至少一个匹配 <span class="inlinecode"><span class="id" type="var">s</span></span>, 那么 <span class="inlinecode"><span class="id" type="var">Union</span></span> <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">re<sub>2</sub></span></span> 匹配 <span class="inlinecode"><span class="id" type="var">s</span></span>.

<div class="paragraph"> </div>


</li>
<li> 最后，如果我们写下某个字符串 <span class="inlinecode"><span class="id" type="var">s</span></span> 作为一个字符串序列的连接
        <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">s_1</span></span> <span class="inlinecode">++</span> <span class="inlinecode">...</span> <span class="inlinecode">++</span> <span class="inlinecode"><span class="id" type="var">s_k</span></span>，且表达式 <span class="inlinecode"><span class="id" type="var">re</span></span> 匹配其中每一个字符串 <span class="inlinecode"><span class="id" type="var">s_i</span></span>，那么
        <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span> 匹配 <span class="inlinecode"><span class="id" type="var">s</span></span>。

<div class="paragraph"> </div>

        作为特殊情况，此字符串序列可能为空，因此无论 <span class="inlinecode"><span class="id" type="var">re</span></span> 是什么 <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span> 总是匹配空字符串 <span class="inlinecode">[]</span>。
</li>
</ul>

<div class="paragraph"> </div>

 容易把非形式化的定义翻译为使用 <span class="inlinecode"><span class="id" type="keyword">Inductive</span></span> 的定义：
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">exp_match</span> {<span class="id" type="var">T</span>} : <span class="id" type="var">list</span> <span class="id" type="var">T</span> → <span class="id" type="var">reg_exp</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;| <span class="id" type="var">MEmpty</span> : <span class="id" type="var">exp_match</span> [] <span class="id" type="var">EmptyStr</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">MChar</span> <span class="id" type="var">x</span> : <span class="id" type="var">exp_match</span> [<span class="id" type="var">x</span>] (<span class="id" type="var">Char</span> <span class="id" type="var">x</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">MApp</span> <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">H<sub>1</sub></span> : <span class="id" type="var">exp_match</span> <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">H<sub>2</sub></span> : <span class="id" type="var">exp_match</span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re<sub>2</sub></span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">exp_match</span> (<span class="id" type="var">s<sub>1</sub></span> ++ <span class="id" type="var">s<sub>2</sub></span>) (<span class="id" type="var">App</span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">MUnionL</span> <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">H<sub>1</sub></span> : <span class="id" type="var">exp_match</span> <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">exp_match</span> <span class="id" type="var">s<sub>1</sub></span> (<span class="id" type="var">Union</span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">MUnionR</span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">H<sub>2</sub></span> : <span class="id" type="var">exp_match</span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re<sub>2</sub></span>) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">exp_match</span> <span class="id" type="var">s<sub>2</sub></span> (<span class="id" type="var">Union</span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">MStar0</span> <span class="id" type="var">re</span> : <span class="id" type="var">exp_match</span> [] (<span class="id" type="var">Star</span> <span class="id" type="var">re</span>)<br/>
&nbsp;&nbsp;| <span class="id" type="var">MStarApp</span> <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">H<sub>1</sub></span> : <span class="id" type="var">exp_match</span> <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re</span>)<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;(<span class="id" type="var">H<sub>2</sub></span> : <span class="id" type="var">exp_match</span> <span class="id" type="var">s<sub>2</sub></span> (<span class="id" type="var">Star</span> <span class="id" type="var">re</span>)) :<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">exp_match</span> (<span class="id" type="var">s<sub>1</sub></span> ++ <span class="id" type="var">s<sub>2</sub></span>) (<span class="id" type="var">Star</span> <span class="id" type="var">re</span>).<br/>
</div>

<div class="doc">
出于可读性的考虑，在此我们也展示使用推断规则表示的定义。
    于此同时，我们引入可读性更好的中缀表示法。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Notation</span> "s =~ re" := (<span class="id" type="var">exp_match</span> <span class="id" type="var">s</span> <span class="id" type="var">re</span>) (<span class="id" type="tactic">at</span> <span class="id" type="var">level</span> 80).<br/>
</div>

<div class="doc">
<center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (MEmpty) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">[]&nbsp;=~&nbsp;EmptyStr</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (MChar) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">[x]&nbsp;=~&nbsp;Char&nbsp;x</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">s<sub>1</sub>&nbsp;=~&nbsp;re<sub>1</sub>&nbsp;&nbsp;&nbsp;&nbsp;s<sub>2</sub>&nbsp;=~&nbsp;re<sub>2</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (MApp) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">s<sub>1</sub>&nbsp;++&nbsp;s<sub>2</sub>&nbsp;=~&nbsp;App&nbsp;re<sub>1</sub>&nbsp;re<sub>2</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">s<sub>1</sub>&nbsp;=~&nbsp;re<sub>1</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (MUnionL) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">s<sub>1</sub>&nbsp;=~&nbsp;Union&nbsp;re<sub>1</sub>&nbsp;re<sub>2</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">s<sub>2</sub>&nbsp;=~&nbsp;re<sub>2</sub></td>
  <td class="infrulenamecol" rowspan="3">
    (MUnionR) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">s<sub>2</sub>&nbsp;=~&nbsp;Union&nbsp;re<sub>1</sub>&nbsp;re<sub>2</sub></td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">&nbsp;&nbsp;</td>
  <td class="infrulenamecol" rowspan="3">
    (MStar0) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">[]&nbsp;=~&nbsp;Star&nbsp;re</td>
  <td></td>
</td>
</table></center><center><table class="infrule">
<tr class="infruleassumption">
  <td class="infrule">s<sub>1</sub>&nbsp;=~&nbsp;re&nbsp;&nbsp;&nbsp;&nbsp;s<sub>2</sub>&nbsp;=~&nbsp;Star&nbsp;re</td>
  <td class="infrulenamecol" rowspan="3">
    (MStarApp) &nbsp;
  </td></tr>
<tr class="infrulemiddle">
  <td class="infrule"><hr /></td>
</tr>
<tr class="infruleassumption">
  <td class="infrule">s<sub>1</sub>&nbsp;++&nbsp;s<sub>2</sub>&nbsp;=~&nbsp;Star&nbsp;re</td>
  <td></td>
</td>
</table></center>
<div class="paragraph"> </div>

 请注意这些规则不<b>完全</b>等同于之前给出的非形式化定义。
    首先，我们并不需要一个规则来直接表述无字符串匹配 <span class="inlinecode"><span class="id" type="var">EmptySet</span></span>；
    我们做的仅仅是不囊括任何可能导致有字符串被 <span class="inlinecode"><span class="id" type="var">EmptySet</span></span> 所匹配的规则。
    （的确，归纳定义的语法并不<b>允许</b>我们表达类似的“否定规则”（negative rule））。

<div class="paragraph"> </div>

    其次，非形式化定义中的 <span class="inlinecode"><span class="id" type="var">Union</span></span> 和 <span class="inlinecode"><span class="id" type="var">Star</span></span> 各自对应了两个构造子：
    <span class="inlinecode"><span class="id" type="var">MUnionL</span></span> / <span class="inlinecode"><span class="id" type="var">MUnionR</span></span>，和 <span class="inlinecode"><span class="id" type="var">MStar0</span></span> / <span class="inlinecode"><span class="id" type="var">MStarApp</span></span>。这在逻辑上等价于
    原始的定义，但在 Coq 中这样更加方便，因为递归出现的 <span class="inlinecode"><span class="id" type="var">exp_match</span></span>
    是作为构造子的直接参数给定的，这在对证据进行归纳时更简单。
    （练习 <span class="inlinecode"><span class="id" type="var">exp_match_ex<sub>1</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">exp_match_ex<sub>2</sub></span></span> 会要求你证明归纳定义中的构造子
    和从非形式化规则的表述中提炼的规则确实是等价的。）

<div class="paragraph"> </div>

    接下来我们对一些例子使用这些规则： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">reg_exp_ex<sub>1</sub></span> : [1] =~ <span class="id" type="var">Char</span> 1.<br/>
<div class="togglescript" id="proofcontrol1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')"><span class="show"></span></div>
<div class="proofscript" id="proof1" onclick="toggleDisplay('proof1');toggleDisplay('proofcontrol1')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">MChar</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">reg_exp_ex<sub>2</sub></span> : [1; 2] =~ <span class="id" type="var">App</span> (<span class="id" type="var">Char</span> 1) (<span class="id" type="var">Char</span> 2).<br/>
<div class="togglescript" id="proofcontrol2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')"><span class="show"></span></div>
<div class="proofscript" id="proof2" onclick="toggleDisplay('proof2');toggleDisplay('proofcontrol2')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> (<span class="id" type="var">MApp</span> [1] <span class="id" type="var">_</span> [2]).<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">apply</span> <span class="id" type="var">MChar</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">apply</span> <span class="id" type="var">MChar</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
（请注意，后一个例子对字符串 <span class="inlinecode">[1]</span> 和 <span class="inlinecode">[2]</span> 直接应用了 <span class="inlinecode"><span class="id" type="var">MApp</span></span>。
    由于目标的形式是 <span class="inlinecode">[1;</span> <span class="inlinecode">2]</span> 而非 <span class="inlinecode">[1]</span> <span class="inlinecode">++</span> <span class="inlinecode">[2]</span>，Coq 并不知道如何分解这个字符串。）

<div class="paragraph"> </div>

    使用 <span class="inlinecode"><span class="id" type="tactic">inversion</span></span>，我们还可以证明某些字符串<b>不</b>匹配一个正则表达式： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">reg_exp_ex<sub>3</sub></span> : ¬([1; 2] =~ <span class="id" type="var">Char</span> 1).<br/>
<div class="togglescript" id="proofcontrol3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')"><span class="show"></span></div>
<div class="proofscript" id="proof3" onclick="toggleDisplay('proof3');toggleDisplay('proofcontrol3')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
我们可以定义一些辅助函数来简化正则表达式的书写。函数 <span class="inlinecode"><span class="id" type="var">reg_exp_of_list</span></span>
    接受一个列表做参数，并构造一个正则表达式来精确地匹配这个列表：
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">reg_exp_of_list</span> {<span class="id" type="var">T</span>} (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">T</span>) :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">l</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| [] ⇒ <span class="id" type="var">EmptyStr</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">x</span> :: <span class="id" type="var">l'</span> ⇒ <span class="id" type="var">App</span> (<span class="id" type="var">Char</span> <span class="id" type="var">x</span>) (<span class="id" type="var">reg_exp_of_list</span> <span class="id" type="var">l'</span>)<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">reg_exp_ex<sub>4</sub></span> : [1; 2; 3] =~ <span class="id" type="var">reg_exp_of_list</span> [1; 2; 3].<br/>
<div class="togglescript" id="proofcontrol4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')"><span class="show"></span></div>
<div class="proofscript" id="proof4" onclick="toggleDisplay('proof4');toggleDisplay('proofcontrol4')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">apply</span> (<span class="id" type="var">MApp</span> [1]).<br/>
&nbsp;&nbsp;{ <span class="id" type="tactic">apply</span> <span class="id" type="var">MChar</span>. }<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> (<span class="id" type="var">MApp</span> [2]).<br/>
&nbsp;&nbsp;{ <span class="id" type="tactic">apply</span> <span class="id" type="var">MChar</span>. }<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> (<span class="id" type="var">MApp</span> [3]).<br/>
&nbsp;&nbsp;{ <span class="id" type="tactic">apply</span> <span class="id" type="var">MChar</span>. }<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">MEmpty</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
我们还可以证明一些关于 <span class="inlinecode"><span class="id" type="var">exp_match</span></span> 的性质。比如，下面的引理显示
    任意一个匹配 <span class="inlinecode"><span class="id" type="var">re</span></span> 的字符串 <span class="inlinecode"><span class="id" type="var">s</span></span> 也匹配 <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span>。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">MStar1</span> :<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> <span class="id" type="var">s</span> (<span class="id" type="var">re</span> : @<span class="id" type="var">reg_exp</span> <span class="id" type="var">T</span>) ,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">s</span> =~ <span class="id" type="var">re</span> →<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">s</span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span>.<br/>
<div class="togglescript" id="proofcontrol5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')"><span class="show"></span></div>
<div class="proofscript" id="proof5" onclick="toggleDisplay('proof5');toggleDisplay('proofcontrol5')">
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">T</span> <span class="id" type="var">s</span> <span class="id" type="var">re</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> &lt;- (<span class="id" type="var">app_nil_r</span> <span class="id" type="var">_</span> <span class="id" type="var">s</span>).<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> (<span class="id" type="var">MStarApp</span> <span class="id" type="var">s</span> [] <span class="id" type="var">re</span>).<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">apply</span> <span class="id" type="var">MStar0</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>
</div>

<div class="doc">
（请注意对 <span class="inlinecode"><span class="id" type="var">app_nil_r</span></span> 的使用改变了目标，以此可匹配 <span class="inlinecode"><span class="id" type="var">MStarApp</span></span> 所需要的形式。）
<div class="paragraph"> </div>

<a name="lab228"></a><h4 class="section">练习：3 星, standard (exp_match_ex<sub>1</sub>)</h4>
 下面的引理显示从形式化的归纳定义中可以得到本章开始的非形式化匹配规则。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">empty_is_empty</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">s</span> : <span class="id" type="var">list</span> <span class="id" type="var">T</span>),<br/>
&nbsp;&nbsp;¬(<span class="id" type="var">s</span> =~ <span class="id" type="var">EmptySet</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">MUnion'</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">s</span> : <span class="id" type="var">list</span> <span class="id" type="var">T</span>) (<span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span> : @<span class="id" type="var">reg_exp</span> <span class="id" type="var">T</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">s</span> =~ <span class="id" type="var">re<sub>1</sub></span> ∨ <span class="id" type="var">s</span> =~ <span class="id" type="var">re<sub>2</sub></span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">s</span> =~ <span class="id" type="var">Union</span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
接下来的引理使用了 <a href="Poly.html"><span class="inlineref">Poly</span></a> 一章中出现的 <span class="inlinecode"><span class="id" type="var">fold</span></span> 函数：
    如果 <span class="inlinecode"><span class="id" type="var">ss</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode">(<span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">T</span>)</span> 表示一个字符串序列 <span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span>,</span> <span class="inlinecode">...,</span> <span class="inlinecode"><span class="id" type="var">sn</span></span>，那么
    <span class="inlinecode"><span class="id" type="var">fold</span></span> <span class="inlinecode"><span class="id" type="var">app</span></span> <span class="inlinecode"><span class="id" type="var">ss</span></span> <span class="inlinecode">[]</span> 是将所有字符串连接的结果。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">MStar'</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">ss</span> : <span class="id" type="var">list</span> (<span class="id" type="var">list</span> <span class="id" type="var">T</span>)) (<span class="id" type="var">re</span> : <span class="id" type="var">reg_exp</span>),<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">s</span>, <span class="id" type="var">In</span> <span class="id" type="var">s</span> <span class="id" type="var">ss</span> → <span class="id" type="var">s</span> =~ <span class="id" type="var">re</span>) →<br/>
&nbsp;&nbsp;<span class="id" type="var">fold</span> <span class="id" type="var">app</span> <span class="id" type="var">ss</span> [] =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab229"></a><h4 class="section">练习：4 星, standard, optional (reg_exp_of_list_spec)</h4>
 请证明 <span class="inlinecode"><span class="id" type="var">reg_exp_of_list</span></span> 满足以下规范： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">reg_exp_of_list_spec</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> : <span class="id" type="var">list</span> <span class="id" type="var">T</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">s<sub>1</sub></span> =~ <span class="id" type="var">reg_exp_of_list</span> <span class="id" type="var">s<sub>2</sub></span> ↔ <span class="id" type="var">s<sub>1</sub></span> = <span class="id" type="var">s<sub>2</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 由于 <span class="inlinecode"><span class="id" type="var">exp_match</span></span> 以递归方式定义，我们可能会发现
    关于正则表达式的证明常常需要对证据进行归纳。
<div class="paragraph"> </div>

 比如，假设我们想要证明以下显然的结果：如果正则表达式 <span class="inlinecode"><span class="id" type="var">re</span></span> 匹配某个字符串 <span class="inlinecode"><span class="id" type="var">s</span></span>，
    那么 <span class="inlinecode"><span class="id" type="var">s</span></span> 中的所有元素必在 <span class="inlinecode"><span class="id" type="var">re</span></span> 中某处以字符字面量的形式出现。

<div class="paragraph"> </div>

    为了表达这个定理，我们首先定义函数 <span class="inlinecode"><span class="id" type="var">re_chars</span></span> 来列举一个正则表达式中出现的
    所有字符：
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">re_chars</span> {<span class="id" type="var">T</span>} (<span class="id" type="var">re</span> : <span class="id" type="var">reg_exp</span>) : <span class="id" type="var">list</span> <span class="id" type="var">T</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">re</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">EmptySet</span> ⇒ []<br/>
&nbsp;&nbsp;| <span class="id" type="var">EmptyStr</span> ⇒ []<br/>
&nbsp;&nbsp;| <span class="id" type="var">Char</span> <span class="id" type="var">x</span> ⇒ [<span class="id" type="var">x</span>]<br/>
&nbsp;&nbsp;| <span class="id" type="var">App</span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span> ⇒ <span class="id" type="var">re_chars</span> <span class="id" type="var">re<sub>1</sub></span> ++ <span class="id" type="var">re_chars</span> <span class="id" type="var">re<sub>2</sub></span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Union</span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span> ⇒ <span class="id" type="var">re_chars</span> <span class="id" type="var">re<sub>1</sub></span> ++ <span class="id" type="var">re_chars</span> <span class="id" type="var">re<sub>2</sub></span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Star</span> <span class="id" type="var">re</span> ⇒ <span class="id" type="var">re_chars</span> <span class="id" type="var">re</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;/HIDEFROMHTML&nbsp;*)</span><br/>
</div>

<div class="doc">
接下来我们这样陈述此定理： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">in_re_match</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">s</span> : <span class="id" type="var">list</span> <span class="id" type="var">T</span>) (<span class="id" type="var">re</span> : <span class="id" type="var">reg_exp</span>) (<span class="id" type="var">x</span> : <span class="id" type="var">T</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">s</span> =~ <span class="id" type="var">re</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">In</span> <span class="id" type="var">x</span> <span class="id" type="var">s</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">In</span> <span class="id" type="var">x</span> (<span class="id" type="var">re_chars</span> <span class="id" type="var">re</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">T</span> <span class="id" type="var">s</span> <span class="id" type="var">re</span> <span class="id" type="var">x</span> <span class="id" type="var">Hmatch</span> <span class="id" type="var">Hin</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Hmatch</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">as</span> [| <span class="id" type="var">x'</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch1</span> <span class="id" type="var">IH<sub>1</sub></span> <span class="id" type="var">Hmatch2</span> <span class="id" type="var">IH<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch</span> <span class="id" type="var">IH</span> | <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch</span> <span class="id" type="var">IH</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">re</span> | <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re</span> <span class="id" type="var">Hmatch1</span> <span class="id" type="var">IH<sub>1</sub></span> <span class="id" type="var">Hmatch2</span> <span class="id" type="var">IH<sub>2</sub></span>].<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;课上已完成&nbsp;*)</span><br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;MEmpty&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">Hin</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;MChar&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">Hin</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">In_app_iff</span> <span class="id" type="keyword">in</span> *.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">Hin</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">Hin</span> | <span class="id" type="var">Hin</span>].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;In&nbsp;x&nbsp;s<sub>1</sub>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">left</span>. <span class="id" type="tactic">apply</span> (<span class="id" type="var">IH<sub>1</sub></span> <span class="id" type="var">Hin</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;In&nbsp;x&nbsp;s<sub>2</sub>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">right</span>. <span class="id" type="tactic">apply</span> (<span class="id" type="var">IH<sub>2</sub></span> <span class="id" type="var">Hin</span>).<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;MUnionL&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">In_app_iff</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">left</span>. <span class="id" type="tactic">apply</span> (<span class="id" type="var">IH</span> <span class="id" type="var">Hin</span>).<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;MUnionR&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">In_app_iff</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">right</span>. <span class="id" type="tactic">apply</span> (<span class="id" type="var">IH</span> <span class="id" type="var">Hin</span>).<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;MStar0&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">Hin</span>.<br/>
</div>

<div class="doc">
特别关注一下对 <span class="inlinecode"><span class="id" type="var">MStarApp</span></span> 分类的证明。我们得到了<b>两个</b>归纳假设：
    一个适用于 <span class="inlinecode"><span class="id" type="var">x</span></span> 出现在 <span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span></span> 中（当匹配 <span class="inlinecode"><span class="id" type="var">re</span></span> 时），另一个则适用于
    <span class="inlinecode"><span class="id" type="var">x</span></span> 出现在 <span class="inlinecode"><span class="id" type="var">s<sub>2</sub></span></span> 中（当匹配 <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span> 时）。
    这是一个很好的例子来表明为什么我们需要对 <span class="inlinecode"><span class="id" type="var">exp_match</span></span> 的证据而非 <span class="inlinecode"><span class="id" type="var">re</span></span>
    进行归纳：对后者的归纳仅仅提供匹配 <span class="inlinecode"><span class="id" type="var">re</span></span> 的字符串的归纳假设，却无法允许我们对
    <span class="inlinecode"><span class="id" type="var">In</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">s<sub>2</sub></span></span> 分类进行推理。 
</div>
<div class="code code-tight">

&nbsp;&nbsp;- <span class="comment">(*&nbsp;MStarApp&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">In_app_iff</span> <span class="id" type="keyword">in</span> <span class="id" type="var">Hin</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">destruct</span> <span class="id" type="var">Hin</span> <span class="id" type="keyword">as</span> [<span class="id" type="var">Hin</span> | <span class="id" type="var">Hin</span>].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;In&nbsp;x&nbsp;s<sub>1</sub>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> (<span class="id" type="var">IH<sub>1</sub></span> <span class="id" type="var">Hin</span>).<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;In&nbsp;x&nbsp;s<sub>2</sub>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> (<span class="id" type="var">IH<sub>2</sub></span> <span class="id" type="var">Hin</span>).<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab230"></a><h4 class="section">练习：4 星, standard (re_not_empty)</h4>
 请编写一个递归函数 <span class="inlinecode"><span class="id" type="var">re_not_empty</span></span> 用来测试某个正则表达式是否会匹配一些字符串。
    并证明你的函数是正确的。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">re_not_empty</span> {<span class="id" type="var">T</span> : <span class="id" type="keyword">Type</span>} (<span class="id" type="var">re</span> : @<span class="id" type="var">reg_exp</span> <span class="id" type="var">T</span>) : <span class="id" type="var">bool</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">re_not_empty_correct</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">re</span> : @<span class="id" type="var">reg_exp</span> <span class="id" type="var">T</span>),<br/>
&nbsp;&nbsp;(<span style='font-size:120%;'>&exist;</span><span class="id" type="var">s</span>, <span class="id" type="var">s</span> =~ <span class="id" type="var">re</span>) ↔ <span class="id" type="var">re_not_empty</span> <span class="id" type="var">re</span> = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab231"></a><h2 class="section"><span class="inlinecode"><span class="id" type="var">remember</span></span> 策略</h2>

<div class="paragraph"> </div>

 <span class="inlinecode"><span class="id" type="tactic">induction</span></span> 策略让人困惑的一个特点是它会接受任意一个项并尝试归纳，
    即使这个项不够一般（general）。其副作用是会丢失掉一些信息（类似没有 <span class="inlinecode"><span class="id" type="var">eqn</span>:</span>
    从句的 <span class="inlinecode"><span class="id" type="tactic">destruct</span></span>），并且使你无法完成证明。比如： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">star_app</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> : <span class="id" type="var">list</span> <span class="id" type="var">T</span>) (<span class="id" type="var">re</span> : @<span class="id" type="var">reg_exp</span> <span class="id" type="var">T</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">s<sub>1</sub></span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">s<sub>2</sub></span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">s<sub>1</sub></span> ++ <span class="id" type="var">s<sub>2</sub></span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">T</span> <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re</span> <span class="id" type="var">H<sub>1</sub></span>.<br/>
</div>

<div class="doc">
仅仅对 <span class="inlinecode"><span class="id" type="var">H<sub>1</sub></span></span> 反演并不会对处理含有递归的分类有太多帮助。（尝试一下！）
    因此我们需要对证据进行归纳！下面是一个朴素的尝试：
</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">H<sub>1</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">as</span> [|<span class="id" type="var">x'</span>|<span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub>'</span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch1</span> <span class="id" type="var">IH<sub>1</sub></span> <span class="id" type="var">Hmatch2</span> <span class="id" type="var">IH<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch</span> <span class="id" type="var">IH</span>|<span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub>'</span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch</span> <span class="id" type="var">IH</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<span class="id" type="var">re''</span>|<span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub>'</span> <span class="id" type="var">re''</span> <span class="id" type="var">Hmatch1</span> <span class="id" type="var">IH<sub>1</sub></span> <span class="id" type="var">Hmatch2</span> <span class="id" type="var">IH<sub>2</sub></span>].<br/>
</div>

<div class="doc">
现在，尽管我们得到了七个分类（正由我们从 <span class="inlinecode"><span class="id" type="var">exp_match</span></span> 的定义中期待的那样），
    但 <span class="inlinecode"><span class="id" type="var">H<sub>1</sub></span></span> 还是丢失了一个非常重要的信息：<span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span></span> 事实上匹配了某种形式的 <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span>。
    这意味着对于<b>全部</b>的七个构造子分类我们都需要给出证明，尽管其中两个（<span class="inlinecode"><span class="id" type="var">MStar0</span></span>
    和 <span class="inlinecode"><span class="id" type="var">MStarApp</span></span>）是自相矛盾的。
    我们仍然可以在一些构造子上继续证明，比如 <span class="inlinecode"><span class="id" type="var">MEmpty</span></span>…… 
</div>
<div class="code code-tight">

&nbsp;&nbsp;- <span class="comment">(*&nbsp;MEmpty&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
</div>

<div class="doc">
……但有一些分类我们却卡住了。比如，对于 <span class="inlinecode"><span class="id" type="var">MChar</span></span> 我们需要证明

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">s<sub>2</sub></span>&nbsp;=~&nbsp;<span class="id" type="var">Char</span>&nbsp;<span class="id" type="var">x'</span>&nbsp;→&nbsp;<span class="id" type="var">x'</span>&nbsp;::&nbsp;<span class="id" type="var">s<sub>2</sub></span>&nbsp;=~&nbsp;<span class="id" type="var">Char</span>&nbsp;<span class="id" type="var">x'</span>,
<div class="paragraph"> </div>

</div>
    这显然是不可能完成的。 
</div>
<div class="code code-tight">

&nbsp;&nbsp;- <span class="comment">(*&nbsp;MChar.&nbsp;卡住了……&nbsp;*)</span><br/>
<span class="id" type="keyword">Abort</span>.<br/>
</div>

<div class="doc">
问题是，只有当 <span class="inlinecode"><span class="id" type="keyword">Prop</span></span> 的假设是完全一般的时候，对其使用 <span class="inlinecode"><span class="id" type="tactic">induction</span></span> 的才会起作用，
    也即，我们需要其所有的参数都是变量，而非更复杂的表达式，比如 <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span>。

<div class="paragraph"> </div>

    （由此，对证据使用 <span class="inlinecode"><span class="id" type="tactic">induction</span></span> 的行为更像是没有 <span class="inlinecode"><span class="id" type="var">eqn</span>:</span> 的 <span class="inlinecode"><span class="id" type="tactic">destruct</span></span>
    而非 <span class="inlinecode"><span class="id" type="tactic">inversion</span></span>。）

<div class="paragraph"> </div>

    解决此问题的一种直接的方式是“手动推广”这个有问题的表达式，
    即为此引理添加一个显式的等式： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">star_app</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> : <span class="id" type="var">list</span> <span class="id" type="var">T</span>) (<span class="id" type="var">re</span> <span class="id" type="var">re'</span> : <span class="id" type="var">reg_exp</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">re'</span> = <span class="id" type="var">Star</span> <span class="id" type="var">re</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">s<sub>1</sub></span> =~ <span class="id" type="var">re'</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">s<sub>2</sub></span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">s<sub>1</sub></span> ++ <span class="id" type="var">s<sub>2</sub></span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span>.<br/>
</div>

<div class="doc">
我们现在可以直接对证据进行归纳，因为第一个假设的参数已经足够一般，
    这意味着我们可以通过反演当前上下文中的 <span class="inlinecode"><span class="id" type="var">re'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span> 来消解掉多数分类。

<div class="paragraph"> </div>

    这在 Coq 中是一种常用的技巧，因此 Coq 提供了策略来自动生成这种等式，
    并且我们也不必改写定理的陈述。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Abort</span>.<br/>
</div>

<div class="doc">
在 Coq 中调用 <span class="inlinecode"><span class="id" type="var">remember</span></span> <span class="inlinecode"><span class="id" type="var">e</span></span> <span class="inlinecode"><span class="id" type="keyword">as</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> 策略会（1）替换所有表达式 <span class="inlinecode"><span class="id" type="var">e</span></span> 为变量 <span class="inlinecode"><span class="id" type="var">x</span></span>，
    （2）在当前上下文中添加一个等式 <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">e</span></span>。我们可以这样使用 <span class="inlinecode"><span class="id" type="var">remember</span></span>
    来证明上面的结果： 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">star_app</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> : <span class="id" type="var">list</span> <span class="id" type="var">T</span>) (<span class="id" type="var">re</span> : <span class="id" type="var">reg_exp</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">s<sub>1</sub></span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">s<sub>2</sub></span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">s<sub>1</sub></span> ++ <span class="id" type="var">s<sub>2</sub></span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">T</span> <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re</span> <span class="id" type="var">H<sub>1</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="var">remember</span> (<span class="id" type="var">Star</span> <span class="id" type="var">re</span>) <span class="id" type="keyword">as</span> <span class="id" type="var">re'</span>.<br/>
</div>

<div class="doc">
我们现在有 <span class="inlinecode"><span class="id" type="var">Heqre'</span></span> <span class="inlinecode">:</span> <span class="inlinecode"><span class="id" type="var">re'</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span>. 
</div>
<div class="code code-tight">

&nbsp;&nbsp;<span class="id" type="tactic">generalize</span> <span class="id" type="tactic">dependent</span> <span class="id" type="var">s<sub>2</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">H<sub>1</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">as</span> [|<span class="id" type="var">x'</span>|<span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub>'</span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch1</span> <span class="id" type="var">IH<sub>1</sub></span> <span class="id" type="var">Hmatch2</span> <span class="id" type="var">IH<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch</span> <span class="id" type="var">IH</span>|<span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub>'</span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch</span> <span class="id" type="var">IH</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;|<span class="id" type="var">re''</span>|<span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub>'</span> <span class="id" type="var">re''</span> <span class="id" type="var">Hmatch1</span> <span class="id" type="var">IH<sub>1</sub></span> <span class="id" type="var">Hmatch2</span> <span class="id" type="var">IH<sub>2</sub></span>].<br/>
</div>

<div class="doc">
 <span class="inlinecode"><span class="id" type="var">Heqre'</span></span> 与多数分类相互矛盾，因此我们可以直接结束这些分类。
</div>
<div class="code code-tight">

&nbsp;&nbsp;- <span class="comment">(*&nbsp;MEmpty&nbsp;*)</span>  <span class="id" type="tactic">discriminate</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;MChar&nbsp;*)</span>   <span class="id" type="tactic">discriminate</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;MApp&nbsp;*)</span>    <span class="id" type="tactic">discriminate</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;MUnionL&nbsp;*)</span> <span class="id" type="tactic">discriminate</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;MUnionR&nbsp;*)</span> <span class="id" type="tactic">discriminate</span>.<br/>
</div>

<div class="doc">
值得注意的分类是 <span class="inlinecode"><span class="id" type="var">Star</span></span>。请注意 <span class="inlinecode"><span class="id" type="var">MStarApp</span></span> 分类的归纳假设 <span class="inlinecode"><span class="id" type="var">IH<sub>2</sub></span></span>
    包含到一个额外的前提 <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re''</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re'</span></span>，这是由 <span class="inlinecode"><span class="id" type="var">remember</span></span>
    所添加的等式所产生的。
</div>
<div class="code code-tight">

&nbsp;&nbsp;- <span class="comment">(*&nbsp;MStar0&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">injection</span> <span class="id" type="var">Heqre'</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">Heqre''</span> <span class="id" type="var">s</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/><hr class='doublespaceincode'/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;MStarApp&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">injection</span> <span class="id" type="var">Heqre'</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">H<sub>0</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">H<sub>1</sub></span>. <span class="id" type="tactic">rewrite</span> &lt;- <span class="id" type="var">app_assoc</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">MStarApp</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="tactic">apply</span> <span class="id" type="var">Hmatch1</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="tactic">apply</span> <span class="id" type="var">IH<sub>2</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="id" type="tactic">rewrite</span> <span class="id" type="var">H<sub>0</sub></span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;* <span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>1</sub></span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab232"></a><h4 class="section">练习：4 星, standard, optional (exp_match_ex<sub>2</sub>)</h4>

<div class="paragraph"> </div>

 下面的引理 <span class="inlinecode"><span class="id" type="var">MStar''</span></span>（以及它的逆，之前的练习题中的 <span class="inlinecode"><span class="id" type="var">MStar'</span></span>）显示
    <span class="inlinecode"><span class="id" type="var">exp_match</span></span> 中 <span class="inlinecode"><span class="id" type="var">Star</span></span> 的定义等价于前面给出的非形式化定义。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">MStar''</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">s</span> : <span class="id" type="var">list</span> <span class="id" type="var">T</span>) (<span class="id" type="var">re</span> : <span class="id" type="var">reg_exp</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">s</span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span> →<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">ss</span> : <span class="id" type="var">list</span> (<span class="id" type="var">list</span> <span class="id" type="var">T</span>),<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">s</span> = <span class="id" type="var">fold</span> <span class="id" type="var">app</span> <span class="id" type="var">ss</span> []<br/>
&nbsp;&nbsp;&nbsp;&nbsp;∧ <span style='font-size:120%;'>&forall;</span><span class="id" type="var">s'</span>, <span class="id" type="var">In</span> <span class="id" type="var">s'</span> <span class="id" type="var">ss</span> → <span class="id" type="var">s'</span> =~ <span class="id" type="var">re</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab233"></a><h4 class="section">练习：5 星, advanced (pumping)</h4>
 正则表达式中一个非常有趣的定理叫做<b>泵引理（Pumping Lemma）</b>，
    非形式化地来讲，它陈述了任意某个足够长的字符串 <span class="inlinecode"><span class="id" type="var">s</span></span> 若匹配一个正则表达式 <span class="inlinecode"><span class="id" type="var">re</span></span>，
    则可以被抽取（pumped）——将 <span class="inlinecode"><span class="id" type="var">s</span></span> 的某个中间部分重复任意次产生的新字符串
    仍然匹配 <span class="inlinecode"><span class="id" type="var">re</span></span>。

<div class="paragraph"> </div>

    我们首先定义什么是“足够长”。由于 Coq 中使用的是构造性逻辑，我们事实上需要计算
    对于任何一个正则表达式 <span class="inlinecode"><span class="id" type="var">re</span></span> 其最小的“可被抽取（pumpability）”长度。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Module</span> <span class="id" type="var">Pumping</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">pumping_constant</span> {<span class="id" type="var">T</span>} (<span class="id" type="var">re</span> : @<span class="id" type="var">reg_exp</span> <span class="id" type="var">T</span>) : <span class="id" type="var">nat</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">re</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| <span class="id" type="var">EmptySet</span> ⇒ 0<br/>
&nbsp;&nbsp;| <span class="id" type="var">EmptyStr</span> ⇒ 1<br/>
&nbsp;&nbsp;| <span class="id" type="var">Char</span> <span class="id" type="var">_</span> ⇒ 2<br/>
&nbsp;&nbsp;| <span class="id" type="var">App</span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">pumping_constant</span> <span class="id" type="var">re<sub>1</sub></span> + <span class="id" type="var">pumping_constant</span> <span class="id" type="var">re<sub>2</sub></span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Union</span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span> ⇒<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">pumping_constant</span> <span class="id" type="var">re<sub>1</sub></span> + <span class="id" type="var">pumping_constant</span> <span class="id" type="var">re<sub>2</sub></span><br/>
&nbsp;&nbsp;| <span class="id" type="var">Star</span> <span class="id" type="var">_</span> ⇒ 1<br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/>
</div>

<div class="doc">
接下来，定义辅助函数 <span class="inlinecode"><span class="id" type="var">napp</span></span> 来重复（连接到它自己）一个字符串特定次数。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">napp</span> {<span class="id" type="var">T</span>} (<span class="id" type="var">n</span> : <span class="id" type="var">nat</span>) (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">T</span>) : <span class="id" type="var">list</span> <span class="id" type="var">T</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">n</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| 0 ⇒ []<br/>
&nbsp;&nbsp;| <span class="id" type="var">S</span> <span class="id" type="var">n'</span> ⇒ <span class="id" type="var">l</span> ++ <span class="id" type="var">napp</span> <span class="id" type="var">n'</span> <span class="id" type="var">l</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">napp_plus</span>: <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">n</span> <span class="id" type="var">m</span> : <span class="id" type="var">nat</span>) (<span class="id" type="var">l</span> : <span class="id" type="var">list</span> <span class="id" type="var">T</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">napp</span> (<span class="id" type="var">n</span> + <span class="id" type="var">m</span>) <span class="id" type="var">l</span> = <span class="id" type="var">napp</span> <span class="id" type="var">n</span> <span class="id" type="var">l</span> ++ <span class="id" type="var">napp</span> <span class="id" type="var">m</span> <span class="id" type="var">l</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">T</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span> <span class="id" type="var">l</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">n</span> <span class="id" type="keyword">as</span> [|<span class="id" type="var">n</span> <span class="id" type="var">IHn</span>].<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">IHn</span>, <span class="id" type="var">app_assoc</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
现在，泵引理是说，如果 <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=~</span> <span class="inlinecode"><span class="id" type="var">re</span></span> 且 <span class="inlinecode"><span class="id" type="var">s</span></span> 的长度最小是 <span class="inlinecode"><span class="id" type="var">re</span></span> 的抽取常数（pumping constant），
    那么 <span class="inlinecode"><span class="id" type="var">s</span></span> 可分割成三个子字符串 <span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span></span> <span class="inlinecode">++</span> <span class="inlinecode"><span class="id" type="var">s<sub>2</sub></span></span> <span class="inlinecode">++</span> <span class="inlinecode"><span class="id" type="var">s<sub>3</sub></span></span>，其中 <span class="inlinecode"><span class="id" type="var">s<sub>2</sub></span></span> 可被重复任意次，
    其结果同 <span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">s<sub>3</sub></span></span> 合并后仍然匹配 <span class="inlinecode"><span class="id" type="var">re</span></span>。由于 <span class="inlinecode"><span class="id" type="var">s<sub>2</sub></span></span> 必须为非空字符串，
    这是一种（构造性的）方式来以我们想要的长度生成匹配 <span class="inlinecode"><span class="id" type="var">re</span></span> 的字符串。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">pumping</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">T</span> (<span class="id" type="var">re</span> : @<span class="id" type="var">reg_exp</span> <span class="id" type="var">T</span>) <span class="id" type="var">s</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">s</span> =~ <span class="id" type="var">re</span> →<br/>
&nbsp;&nbsp;<span class="id" type="var">pumping_constant</span> <span class="id" type="var">re</span> ≤ <span class="id" type="var">length</span> <span class="id" type="var">s</span> →<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">s<sub>3</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">s</span> = <span class="id" type="var">s<sub>1</sub></span> ++ <span class="id" type="var">s<sub>2</sub></span> ++ <span class="id" type="var">s<sub>3</sub></span> ∧<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">s<sub>2</sub></span> ≠ [] ∧<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">m</span>, <span class="id" type="var">s<sub>1</sub></span> ++ <span class="id" type="var">napp</span> <span class="id" type="var">m</span> <span class="id" type="var">s<sub>2</sub></span> ++ <span class="id" type="var">s<sub>3</sub></span> =~ <span class="id" type="var">re</span>.<br/>
</div>

<div class="doc">
为了简化证明（也就是接下来你需要填写的），我们使用 <span class="inlinecode"><span class="id" type="keyword">Require</span></span> 来引入 <span class="inlinecode"><span class="id" type="tactic">omega</span></span> 策略，
    其可用于自动化地完成一些自然数等式和不等式的枯燥证明。
    我们在后面的章节中会详细解释 <span class="inlinecode"><span class="id" type="tactic">omega</span></span>，不过在这里请尝试做一些实验。
    下面的第一个归纳分类中展示了如何使用它。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Import</span> <span class="id" type="var">Coq.omega.Omega</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">T</span> <span class="id" type="var">re</span> <span class="id" type="var">s</span> <span class="id" type="var">Hmatch</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">induction</span> <span class="id" type="var">Hmatch</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="keyword">as</span> [ | <span class="id" type="var">x</span> | <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch1</span> <span class="id" type="var">IH<sub>1</sub></span> <span class="id" type="var">Hmatch2</span> <span class="id" type="var">IH<sub>2</sub></span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch</span> <span class="id" type="var">IH</span> | <span class="id" type="var">re<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re<sub>2</sub></span> <span class="id" type="var">Hmatch</span> <span class="id" type="var">IH</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;| <span class="id" type="var">re</span> | <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">s<sub>2</sub></span> <span class="id" type="var">re</span> <span class="id" type="var">Hmatch1</span> <span class="id" type="var">IH<sub>1</sub></span> <span class="id" type="var">Hmatch2</span> <span class="id" type="var">IH<sub>2</sub></span> ].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;MEmpty&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">omega</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">End</span> <span class="id" type="var">Pumping</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 

<div class="doc">
<a name="lab234"></a><h1 class="section">案例学习：改进互映</h1>

<div class="paragraph"> </div>

 在 <a href="Logic.html"><span class="inlineref">Logic</span></a> 一章中，我们经常需要关联起对布尔值的计算和 <span class="inlinecode"><span class="id" type="keyword">Prop</span></span>
    中的陈述，然而进行这样的关联往往会导致冗长的证明。请考虑以下定理的证明：
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">filter_not_empty_In</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">l</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">filter</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">x</span> ⇒ <span class="id" type="var">n</span> =? <span class="id" type="var">x</span>) <span class="id" type="var">l</span> ≠ [] →<br/>
&nbsp;&nbsp;<span class="id" type="var">In</span> <span class="id" type="var">n</span> <span class="id" type="var">l</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">l</span>. <span class="id" type="tactic">induction</span> <span class="id" type="var">l</span> <span class="id" type="keyword">as</span> [|<span class="id" type="var">m</span> <span class="id" type="var">l'</span> <span class="id" type="var">IHl'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;l&nbsp;=&nbsp;<span class="inlinecode"></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;l&nbsp;=&nbsp;m&nbsp;::&nbsp;l'&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">destruct</span> (<span class="id" type="var">n</span> =? <span class="id" type="var">m</span>) <span class="id" type="var">eqn</span>:<span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=?&nbsp;m&nbsp;=&nbsp;true&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">_</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">eqb_eq</span> <span class="id" type="keyword">in</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">left</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=?&nbsp;m&nbsp;=&nbsp;false&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">H'</span>. <span class="id" type="var">right</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">IHl'</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H'</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
在 <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> 后的第一个分支中，我们解构 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=?</span> <span class="inlinecode"><span class="id" type="var">m</span></span>
    后生成的等式显式地使用了 <span class="inlinecode"><span class="id" type="var">eqb_eq</span></span> 引理，以此将假设
    <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=?</span> <span class="inlinecode"><span class="id" type="var">m</span></span> 转换为假设 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span>；接着使用 <span class="inlinecode"><span class="id" type="tactic">rewrite</span></span>
    策略和这个假设来完成此分支的证明。
<div class="paragraph"> </div>

 为了简化这样的证明，我们可定义一个归纳命题，用于对 <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=?</span> <span class="inlinecode"><span class="id" type="var">m</span></span>
    产生更好的分类讨论原理。
    它不会生成类似 <span class="inlinecode">(<span class="id" type="var">n</span></span> <span class="inlinecode">=?</span> <span class="inlinecode"><span class="id" type="var">m</span>)</span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span>这样的等式，因为一般来说对证明并不直接有用，
    其生成的分类讨论原理正是我们所需要的假设: <span class="inlinecode"><span class="id" type="var">n</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">m</span></span>。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">reflect</span> (<span class="id" type="var">P</span> : <span class="id" type="keyword">Prop</span>) : <span class="id" type="var">bool</span> → <span class="id" type="keyword">Prop</span> :=<br/>
| <span class="id" type="var">ReflectT</span> (<span class="id" type="var">H</span> :   <span class="id" type="var">P</span>) : <span class="id" type="var">reflect</span> <span class="id" type="var">P</span> <span class="id" type="var">true</span><br/>
| <span class="id" type="var">ReflectF</span> (<span class="id" type="var">H</span> : ¬<span class="id" type="var">P</span>) : <span class="id" type="var">reflect</span> <span class="id" type="var">P</span> <span class="id" type="var">false</span>.<br/>
</div>

<div class="doc">
性质 <span class="inlinecode"><span class="id" type="var">reflect</span></span> 接受两个参数：一个命题 <span class="inlinecode"><span class="id" type="var">P</span></span> 和一个布尔值 <span class="inlinecode"><span class="id" type="var">b</span></span>。
    直观地讲，它陈述了性质 <span class="inlinecode"><span class="id" type="var">P</span></span> 在布尔值 <span class="inlinecode"><span class="id" type="var">b</span></span> 中所<b>映现</b>（也即，等价）：
    换句话说，<span class="inlinecode"><span class="id" type="var">P</span></span> 成立当且仅当 <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span>。为了理解这一点，请注意定义，
    我们能够产生 <span class="inlinecode"><span class="id" type="var">reflect</span></span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">true</span></span> 的证据的唯一方式是证明 <span class="inlinecode"><span class="id" type="var">P</span></span> 为真并使用
    <span class="inlinecode"><span class="id" type="var">ReflectT</span></span> 构造子。如果我们反转这个陈述，意味着从 <span class="inlinecode"><span class="id" type="var">reflect</span></span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">true</span></span>
    的证明中抽取出 <span class="inlinecode"><span class="id" type="var">P</span></span> 的证据也是可能的。与此类似，证明 <span class="inlinecode"><span class="id" type="var">reflect</span></span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">false</span></span>
    的唯一方式是合并 <span class="inlinecode">¬</span> <span class="inlinecode"><span class="id" type="var">P</span></span> 的证据和 <span class="inlinecode"><span class="id" type="var">ReflectF</span></span> 构造子。

<div class="paragraph"> </div>

    形式化这种直觉并证明 <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode">↔</span> <span class="inlinecode"><span class="id" type="var">b</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">true</span></span> 和 <span class="inlinecode"><span class="id" type="var">reflect</span></span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span>
    这两个表述确实等价是十分容易的。首先是从左到右的蕴含：
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">iff_reflect</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">P</span> <span class="id" type="var">b</span>, (<span class="id" type="var">P</span> ↔ <span class="id" type="var">b</span> = <span class="id" type="var">true</span>) → <span class="id" type="var">reflect</span> <span class="id" type="var">P</span> <span class="id" type="var">b</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;课上已完成&nbsp;*)</span><br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">P</span> <span class="id" type="var">b</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">b</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">apply</span> <span class="id" type="var">ReflectT</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">apply</span> <span class="id" type="var">ReflectF</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">H'</span>. <span class="id" type="tactic">discriminate</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
Now you prove the right-to-left implication: 
<div class="paragraph"> </div>

<a name="lab235"></a><h4 class="section">练习：2 星, standard, recommended (reflect_iff)</h4>

</div>
<div class="code code-space">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">reflect_iff</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">P</span> <span class="id" type="var">b</span>, <span class="id" type="var">reflect</span> <span class="id" type="var">P</span> <span class="id" type="var">b</span> → (<span class="id" type="var">P</span> ↔ <span class="id" type="var">b</span> = <span class="id" type="var">true</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 使用 <span class="inlinecode"><span class="id" type="var">reflect</span></span> 而非“当且仅当”连词的好处是，通过解构一个形如
    <span class="inlinecode"><span class="id" type="var">reflect</span></span> <span class="inlinecode"><span class="id" type="var">P</span></span> <span class="inlinecode"><span class="id" type="var">b</span></span> 的假设或引理，我们可以对 <span class="inlinecode"><span class="id" type="var">b</span></span>
    进行分类讨论，同时为两个分支（第一个子目标中的 <span class="inlinecode"><span class="id" type="var">P</span></span>
    和第二个中的 <span class="inlinecode">¬</span> <span class="inlinecode"><span class="id" type="var">P</span></span>）生成适当的假设。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">eqbP</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">m</span>, <span class="id" type="var">reflect</span> (<span class="id" type="var">n</span> = <span class="id" type="var">m</span>) (<span class="id" type="var">n</span> =? <span class="id" type="var">m</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">iff_reflect</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">eqb_eq</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<span class="inlinecode"><span class="id" type="var">filter_not_empty_In</span></span> 的一种更流畅证明如下所示。请注意对 <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> 和 <span class="inlinecode"><span class="id" type="tactic">apply</span></span>
    的使用是如何合并成一个 <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> 的使用。 
<div class="paragraph"> </div>

 （为了更清晰地看到这点，使用 Coq 查看 <span class="inlinecode"><span class="id" type="var">filter_not_empty_In</span></span>
    的两个证明，并观察在 <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> 的第一个分类开始时证明状态的区别。） 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">filter_not_empty_In'</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">l</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">filter</span> (<span class="id" type="keyword">fun</span> <span class="id" type="var">x</span> ⇒ <span class="id" type="var">n</span> =? <span class="id" type="var">x</span>) <span class="id" type="var">l</span> ≠ [] →<br/>
&nbsp;&nbsp;<span class="id" type="var">In</span> <span class="id" type="var">n</span> <span class="id" type="var">l</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">n</span> <span class="id" type="var">l</span>. <span class="id" type="tactic">induction</span> <span class="id" type="var">l</span> <span class="id" type="keyword">as</span> [|<span class="id" type="var">m</span> <span class="id" type="var">l'</span> <span class="id" type="var">IHl'</span>].<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;l&nbsp;=&nbsp;<span class="inlinecode"></span>&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">intros</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="comment">(*&nbsp;l&nbsp;=&nbsp;m&nbsp;::&nbsp;l'&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">simpl</span>. <span class="id" type="tactic">destruct</span> (<span class="id" type="var">eqbP</span> <span class="id" type="var">n</span> <span class="id" type="var">m</span>) <span class="id" type="keyword">as</span> [<span class="id" type="var">H</span> | <span class="id" type="var">H</span>].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;=&nbsp;m&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">_</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span>. <span class="id" type="var">left</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="comment">(*&nbsp;n&nbsp;&lt;&gt;&nbsp;m&nbsp;*)</span><br/>
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">H'</span>. <span class="id" type="var">right</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">IHl'</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H'</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab236"></a><h4 class="section">练习：3 星, standard, recommended (eqbP_practice)</h4>
 使用上面的 <span class="inlinecode"><span class="id" type="var">eqbP</span></span> 证明以下定理：
</div>
<div class="code code-tight">

<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">count</span> <span class="id" type="var">n</span> <span class="id" type="var">l</span> :=<br/>
&nbsp;&nbsp;<span class="id" type="keyword">match</span> <span class="id" type="var">l</span> <span class="id" type="keyword">with</span><br/>
&nbsp;&nbsp;| [] ⇒ 0<br/>
&nbsp;&nbsp;| <span class="id" type="var">m</span> :: <span class="id" type="var">l'</span> ⇒ (<span class="id" type="keyword">if</span> <span class="id" type="var">n</span> =? <span class="id" type="var">m</span> <span class="id" type="keyword">then</span> 1 <span class="id" type="keyword">else</span> 0) + <span class="id" type="var">count</span> <span class="id" type="var">n</span> <span class="id" type="var">l'</span><br/>
&nbsp;&nbsp;<span class="id" type="keyword">end</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">eqbP_practice</span> : <span style='font-size:120%;'>&forall;</span><span class="id" type="var">n</span> <span class="id" type="var">l</span>,<br/>
&nbsp;&nbsp;<span class="id" type="var">count</span> <span class="id" type="var">n</span> <span class="id" type="var">l</span> = 0 → ~(<span class="id" type="var">In</span> <span class="id" type="var">n</span> <span class="id" type="var">l</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 这个小例子展示了互映证明可以怎样为我们提供一些便利。在大型的开发中，
    使用 <span class="inlinecode"><span class="id" type="var">reflect</span></span> 往往更容易写出清晰和简短的证明脚本。我们将会在后面的章节
    和<b>编程语言基础</b>一卷中看到更多的例子。

<div class="paragraph"> </div>

    对 <span class="inlinecode"><span class="id" type="var">reflect</span></span> 性质的使用已被 <b>SSReflect</b> 推广开来，这是一个
    Coq 程序库，用于形式化一些数学上的重要结果，包括四色定理和法伊特－汤普森定理。
    SSReflect 的名字代表着 <b>small-scale reflection</b>，也即，普遍性地使用
    互映来简化与布尔值计算有关的证明。
</div>

<div class="doc">
<a name="lab237"></a><h1 class="section">额外练习</h1>

<div class="paragraph"> </div>

<a name="lab238"></a><h4 class="section">练习：3 星, standard, recommended (nostutter_defn)</h4>
 写出性质的归纳定义是本课程中你需要的重要技能。请尝试去独立解决以下的练习。

<div class="paragraph"> </div>

    列表连续地重复某元素称为 "百叶窗式" (stutter)。
    （此概念不同于不包含重复元素：<span class="inlinecode">1;4;1</span> 虽然包含重复元素 <span class="inlinecode">1</span>，
    但因其未连续出现，故不是百叶窗式列表）。
    <span class="inlinecode"><span class="id" type="var">nostutter</span></span> <span class="inlinecode"><span class="id" type="var">mylist</span></span> 表示 <span class="inlinecode"><span class="id" type="var">mylist</span></span> 不是百叶窗式列表。
    请写出 <span class="inlinecode"><span class="id" type="var">nostutter</span></span> 的归纳定义。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">nostutter</span> {<span class="id" type="var">X</span>:<span class="id" type="keyword">Type</span>} : <span class="id" type="var">list</span> <span class="id" type="var">X</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
.<br/>
</div>

<div class="doc">
请确保以下测试成功，但如果你觉得我们建议的证明（在注释中）并不有效，也可随意更改他们。
    若你的定义与我们的不同，也可能仍然是正确的，但在这种情况下可能需要不同的证明。
    （你会注意到建议的证明中使用了一些我们尚未讨论过的策略，这可以让证明适用于不同的 <span class="inlinecode"><span class="id" type="var">nostutter</span></span>
    定义方式。你可以取消注释并直接使用他们，也可以用基础的策略证明这些例子。） 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Example</span> <span class="id" type="var">test_nostutter_1</span>: <span class="id" type="var">nostutter</span> [3;1;4;1;5;6].<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
<span class="comment">(*&nbsp;<br/>
&nbsp;&nbsp;Proof.&nbsp;repeat&nbsp;constructor;&nbsp;apply&nbsp;eqb_neq;&nbsp;auto.<br/>
&nbsp;&nbsp;Qed.<br/>
*)</span><br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_nostutter_2</span>:  <span class="id" type="var">nostutter</span> (@<span class="id" type="var">nil</span> <span class="id" type="var">nat</span>).<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
<span class="comment">(*&nbsp;<br/>
&nbsp;&nbsp;Proof.&nbsp;repeat&nbsp;constructor;&nbsp;apply&nbsp;eqb_neq;&nbsp;auto.<br/>
&nbsp;&nbsp;Qed.<br/>
*)</span><br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_nostutter_3</span>:  <span class="id" type="var">nostutter</span> [5].<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
<span class="comment">(*&nbsp;<br/>
&nbsp;&nbsp;Proof.&nbsp;repeat&nbsp;constructor;&nbsp;apply&nbsp;eqb_false;&nbsp;auto.&nbsp;Qed.<br/>
*)</span><br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_nostutter_4</span>:      <span class="id" type="var">not</span> (<span class="id" type="var">nostutter</span> [3;1;1;4]).<br/>
<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
<span class="comment">(*&nbsp;<br/>
&nbsp;&nbsp;Proof.&nbsp;intro.<br/>
&nbsp;&nbsp;repeat&nbsp;match&nbsp;goal&nbsp;with<br/>
&nbsp;&nbsp;&nbsp;&nbsp;h:&nbsp;nostutter&nbsp;_&nbsp;&#x22A2;&nbsp;_&nbsp;=&gt;&nbsp;inversion&nbsp;h;&nbsp;clear&nbsp;h;&nbsp;subst<br/>
&nbsp;&nbsp;end.<br/>
&nbsp;&nbsp;contradiction&nbsp;Hneq0;&nbsp;auto.&nbsp;Qed.<br/>
*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_nostutter</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab239"></a><h4 class="section">练习：4 星, advanced (filter_challenge)</h4>
 让我们证明在 <span class="inlinecode"><span class="id" type="var">Poly</span></span> 一章中 <span class="inlinecode"><span class="id" type="var">filter</span></span> 的定义匹配某个抽象的规范。
    可以这样非形式化地描述这个规范：

<div class="paragraph"> </div>

    列表 <span class="inlinecode"><span class="id" type="var">l</span></span> 是一个 <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span> 的“顺序合并”（in-order merge），如果它以
    <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span> 中元素的顺序包含 <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span> 中的所有元素，尽管可能是交替的。比如：

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;[1;4;6;2;3]
<div class="paragraph"> </div>

</div>
    是

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;[1;6;2]
<div class="paragraph"> </div>

</div>
    和

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;[4;3].
<div class="paragraph"> </div>

</div>
    的顺序合并。

<div class="paragraph"> </div>

    现在，假设我们有集合 <span class="inlinecode"><span class="id" type="var">X</span></span>，函数 <span class="inlinecode"><span class="id" type="var">test</span>:</span> <span class="inlinecode"><span class="id" type="var">X</span>→<span class="id" type="var">bool</span></span> 和一个类型为 <span class="inlinecode"><span class="id" type="var">list</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> 的列表
    <span class="inlinecode"><span class="id" type="var">l</span></span>。接着接设如果 <span class="inlinecode"><span class="id" type="var">l</span></span> 是 <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> 和 <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span> 的顺序合并，且 <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> 中的每个元素满足 <span class="inlinecode"><span class="id" type="var">test</span></span>，
    而 <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span> 中没有元素满足 <span class="inlinecode"><span class="id" type="var">test</span></span>，那么 <span class="inlinecode"><span class="id" type="var">filter</span></span> <span class="inlinecode"><span class="id" type="var">test</span></span> <span class="inlinecode"><span class="id" type="var">l</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span>。

<div class="paragraph"> </div>

    请将这段规范翻译为 Coq 中的定理并证明它。（你首先需要定义合并两个列表的含义是什么。
    请使用归纳关系而非 <span class="inlinecode"><span class="id" type="keyword">Fixpoint</span></span> 来完成。）
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_filter_challenge</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab240"></a><h4 class="section">练习：5 星, advanced, optional (filter_challenge_2)</h4>
 另一种刻画 <span class="inlinecode"><span class="id" type="var">filter</span></span> 行为的方式是：在 <span class="inlinecode"><span class="id" type="var">l</span></span> 的所有其元素满足 <span class="inlinecode"><span class="id" type="var">test</span></span> 的子序列中，
    <span class="inlinecode"><span class="id" type="var">filter</span></span> <span class="inlinecode"><span class="id" type="var">test</span></span> <span class="inlinecode"><span class="id" type="var">l</span></span> 是最长的那个。请形式化这个命题并证明它。
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab241"></a><h4 class="section">练习：4 星, standard, optional (palindromes)</h4>
 回文是倒序排列与正序排列相同的序列。

<div class="paragraph"> </div>

<ul class="doclist">
<li> 在 <span class="inlinecode"><span class="id" type="var">listX</span></span> 上定义一个归纳命题 <span class="inlinecode"><span class="id" type="var">pal</span></span> 来表达回文的含义。
      （提示：你需要三个分类。定义应当基于列表的结构；仅仅使用一个构造子，例如

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;<span class="id" type="var">c</span>&nbsp;:&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">l</span>,&nbsp;<span class="id" type="var">l</span>&nbsp;=&nbsp;<span class="id" type="var">rev</span>&nbsp;<span class="id" type="var">l</span>&nbsp;→&nbsp;<span class="id" type="var">pal</span>&nbsp;<span class="id" type="var">l</span>
<div class="paragraph"> </div>

</div>
      看起来十分显而易见，但并不会很好的工作。)

<div class="paragraph"> </div>


</li>
<li> 证明（<span class="inlinecode"><span class="id" type="var">pal_app_rev</span></span>）

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">l</span>,&nbsp;<span class="id" type="var">pal</span>&nbsp;(<span class="id" type="var">l</span>&nbsp;++&nbsp;<span class="id" type="var">rev</span>&nbsp;<span class="id" type="var">l</span>).
<div class="paragraph"> </div>

</div>

</li>
<li> 证明（<span class="inlinecode"><span class="id" type="var">pal_rev</span></span> that）

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">l</span>,&nbsp;<span class="id" type="var">pal</span>&nbsp;<span class="id" type="var">l</span>&nbsp;→&nbsp;<span class="id" type="var">l</span>&nbsp;=&nbsp;<span class="id" type="var">rev</span>&nbsp;<span class="id" type="var">l</span>.
<div class="paragraph"> </div>

</div>

</li>
</ul>

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_pal_pal_app_rev_pal_rev</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab242"></a><h4 class="section">练习：5 星, standard, optional (palindrome_converse)</h4>
 由于缺乏证据，反方向的证明要困难许多。使用之前练习中定义的 <span class="inlinecode"><span class="id" type="var">pal</span></span> 来证明

<div class="paragraph"> </div>

<div class="code code-tight">
&nbsp;&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">l</span>,&nbsp;<span class="id" type="var">l</span>&nbsp;=&nbsp;<span class="id" type="var">rev</span>&nbsp;<span class="id" type="var">l</span>&nbsp;→&nbsp;<span class="id" type="var">pal</span>&nbsp;<span class="id" type="var">l</span>.
<div class="paragraph"> </div>

</div>

</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab243"></a><h4 class="section">练习：4 星, advanced, optional (NoDup)</h4>
 请回忆一下 <span class="inlinecode"><span class="id" type="var">Logic</span></span> 章节中性质 <span class="inlinecode"><span class="id" type="var">In</span></span> 的定义，其断言值 <span class="inlinecode"><span class="id" type="var">x</span></span> 在列表 <span class="inlinecode"><span class="id" type="var">l</span></span> 中至少出现一次：
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;Fixpoint&nbsp;In&nbsp;(A&nbsp;:&nbsp;Type)&nbsp;(x&nbsp;:&nbsp;A)&nbsp;(l&nbsp;:&nbsp;list&nbsp;A)&nbsp;:&nbsp;Prop&nbsp;:=<br/>
&nbsp;&nbsp;&nbsp;match&nbsp;l&nbsp;with<br/>
&nbsp;&nbsp;&nbsp;|&nbsp;<span class="inlinecode"></span>&nbsp;=&gt;&nbsp;False<br/>
&nbsp;&nbsp;&nbsp;|&nbsp;x'&nbsp;::&nbsp;l'&nbsp;=&gt;&nbsp;x'&nbsp;=&nbsp;x&nbsp;\/&nbsp;In&nbsp;A&nbsp;x&nbsp;l'<br/>
&nbsp;&nbsp;&nbsp;end&nbsp;*)</span><br/>
</div>

<div class="doc">
你的第一个任务是使用 <span class="inlinecode"><span class="id" type="var">In</span></span> 来定义命题 <span class="inlinecode"><span class="id" type="var">disjoint</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span>：仅当列表 <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span>
    和 <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span>（元素的类型为 <span class="inlinecode"><span class="id" type="var">X</span></span>）不含有相同的元素时其可被证明。
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<div class="doc">
接下来，使用 <span class="inlinecode"><span class="id" type="var">In</span></span>　定义归纳命题 <span class="inlinecode"><span class="id" type="var">NoDup</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode"><span class="id" type="var">l</span></span>，其可被证明仅当列表 <span class="inlinecode"><span class="id" type="var">l</span></span>
    （元素类型为 <span class="inlinecode"><span class="id" type="var">X</span></span>）的每个元素都不相同。比如，<span class="inlinecode"><span class="id" type="var">NoDup</span></span> <span class="inlinecode"><span class="id" type="var">nat</span></span> <span class="inlinecode">[1;2;3;4]</span>
    和 <span class="inlinecode"><span class="id" type="var">NoDup</span></span> <span class="inlinecode"><span class="id" type="var">bool</span></span> <span class="inlinecode">[]</span> 是可被证明的，然而 <span class="inlinecode"><span class="id" type="var">NoDup</span></span> <span class="inlinecode"><span class="id" type="var">nat</span></span> <span class="inlinecode">[1;2;1]</span>
    和 <span class="inlinecode"><span class="id" type="var">NoDup</span></span> <span class="inlinecode"><span class="id" type="var">bool</span></span> <span class="inlinecode">[<span class="id" type="var">true</span>;<span class="id" type="var">true</span>]</span> 是不行的。
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
</div>

<div class="doc">
最后，使用 <span class="inlinecode"><span class="id" type="var">disjoint</span></span>，<span class="inlinecode"><span class="id" type="var">NoDup</span></span> 和 <span class="inlinecode">++</span>（列表连接）陈述并证明一个或多个有趣的定理。 
</div>
<div class="code code-tight">

<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_NoDup_disjoint_etc</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab244"></a><h4 class="section">练习：4 星, advanced, optional (pigeonhole_principle)</h4>
 _鸽笼原理（Pigeonhole Principle）</b>是一个关于计数的基本事实：
    将超过 <span class="inlinecode"><span class="id" type="var">n</span></span> 个物体放进 <span class="inlinecode"><span class="id" type="var">n</span></span> 个鸽笼，则必有鸽笼包含至少两个物体。
    与此前诸多情形相似，这一数学事实看似乏味，但其证明手段并不平凡，
    如下所述： 
<div class="paragraph"> </div>

 首先容易证明一个有用的引理。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">in_split</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">X</span>:<span class="id" type="keyword">Type</span>) (<span class="id" type="var">x</span>:<span class="id" type="var">X</span>) (<span class="id" type="var">l</span>:<span class="id" type="var">list</span> <span class="id" type="var">X</span>),<br/>
&nbsp;&nbsp;<span class="id" type="var">In</span> <span class="id" type="var">x</span> <span class="id" type="var">l</span> →<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">l<sub>1</sub></span> <span class="id" type="var">l<sub>2</sub></span>, <span class="id" type="var">l</span> = <span class="id" type="var">l<sub>1</sub></span> ++ <span class="id" type="var">x</span> :: <span class="id" type="var">l<sub>2</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
现在请定一个性质 <span class="inlinecode"><span class="id" type="var">repeats</span></span>，使 <span class="inlinecode"><span class="id" type="var">repeats</span></span> <span class="inlinecode"><span class="id" type="var">X</span></span> <span class="inlinecode"><span class="id" type="var">l</span></span> 断言 <span class="inlinecode"><span class="id" type="var">l</span></span>
    包含至少一个（类型为 <span class="inlinecode"><span class="id" type="var">X</span></span> 的）重复的元素。
</div>
<div class="code code-tight">

<span class="id" type="keyword">Inductive</span> <span class="id" type="var">repeats</span> {<span class="id" type="var">X</span>:<span class="id" type="keyword">Type</span>} : <span class="id" type="var">list</span> <span class="id" type="var">X</span> → <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span><br/>
.<br/>
</div>

<div class="doc">
现在，我们这样来形式化鸽笼原理。假设列表 <span class="inlinecode"><span class="id" type="var">l<sub>2</sub></span></span> 表示鸽笼标签的列表，列表 <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span>
    表示标签被指定给一个列表里的元素。如果元素的个数多于标签的个数，那么至少有两个
    元素被指定了同一个标签——也即，列表 <span class="inlinecode"><span class="id" type="var">l<sub>1</sub></span></span> 含有重复元素。

<div class="paragraph"> </div>

    如果使用 <span class="inlinecode"><span class="id" type="var">excluded_middule</span></span> 假设并展示 <span class="inlinecode"><span class="id" type="var">In</span></span> 是可判定的（decidable），
    即 <span class="inlinecode"><span style='font-size:120%;'>&forall;</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">l</span>,</span> <span class="inlinecode">(<span class="id" type="var">In</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">l</span>)</span> <span class="inlinecode">∨</span> <span class="inlinecode">¬</span> <span class="inlinecode">(<span class="id" type="var">In</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">l</span>)</span>，那么这个证明会容易很多。
    然而，若<b>不</b>假设 <span class="inlinecode"><span class="id" type="var">In</span></span> 的可判定性也同样可以证明它；在这样的情况下便不必使用
    <span class="inlinecode"><span class="id" type="var">excluded_middle</span></span> 假设。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Theorem</span> <span class="id" type="var">pigeonhole_principle</span>: <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">X</span>:<span class="id" type="keyword">Type</span>) (<span class="id" type="var">l<sub>1</sub></span>  <span class="id" type="var">l<sub>2</sub></span>:<span class="id" type="var">list</span> <span class="id" type="var">X</span>),<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">excluded_middle</span> →<br/>
&nbsp;&nbsp;&nbsp;(<span style='font-size:120%;'>&forall;</span><span class="id" type="var">x</span>, <span class="id" type="var">In</span> <span class="id" type="var">x</span> <span class="id" type="var">l<sub>1</sub></span> → <span class="id" type="var">In</span> <span class="id" type="var">x</span> <span class="id" type="var">l<sub>2</sub></span>) →<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">length</span> <span class="id" type="var">l<sub>2</sub></span> &lt; <span class="id" type="var">length</span> <span class="id" type="var">l<sub>1</sub></span> →<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="var">repeats</span> <span class="id" type="var">l<sub>1</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">intros</span> <span class="id" type="var">X</span> <span class="id" type="var">l<sub>1</sub></span>. <span class="id" type="tactic">induction</span> <span class="id" type="var">l<sub>1</sub></span> <span class="id" type="keyword">as</span> [|<span class="id" type="var">x</span> <span class="id" type="var">l<sub>1</sub>'</span> <span class="id" type="var">IHl1'</span>].<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/><hr class='doublespaceincode'/>
<span class="comment">(*&nbsp;请勿修改下面这一行：&nbsp;*)</span><br/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">manual_grade_for_check_repeats</span> : <span class="id" type="var">option</span> (<span class="id" type="var">nat</span>*<span class="id" type="var">string</span>) := <span class="id" type="var">None</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab245"></a><h2 class="section">扩展练习：经验证的正则表达式匹配器</h2>

<div class="paragraph"> </div>

 我们现在已经定义了正则表达式的匹配关系和多态列表。我们可以使用这些定义来手动地证明
    给定的正则表达式是否匹配某个字符串，但这并不是一个可以自动地判断是否匹配的程序。

<div class="paragraph"> </div>

    有理由期待，用于构造匹配关系证据的归纳规则可以被翻译为一个递归函数，
    其在正则表达式上的递归对应于这种关系。然而，定义这样的函数并没有那么直接，
    由于给定的正则表达式会被 Coq 识别为递归变量，作为结果，Coq 并不会接受这个函数，
    即使它总是停机。

<div class="paragraph"> </div>

    重度优化的匹配器会将正则表达式翻译为一个状态机，并决定状态机是否接受
    某个字符串。然而，正则表达式匹配也可以通过一个算法来实现，其仅仅操作字符串和
    正则表达式，无需定义和维护额外的数据类型，例如状态机。我们将会实现这样的算法，
    并验证其值与匹配关系是互映的。 
<div class="paragraph"> </div>

 我们将要实现的正则表达式匹配器会匹配由 ASCII 字符构成的列表：
</div>
<div class="code code-tight">
<span class="id" type="keyword">Require</span> <span class="id" type="keyword">Export</span> <span class="id" type="var">Coq.Strings.Ascii</span>.<br/><hr class='doublespaceincode'/>
<span class="id" type="keyword">Definition</span> <span class="id" type="var">string</span> := <span class="id" type="var">list</span> <span class="id" type="var">ascii</span>.<br/>
</div>

<div class="doc">
Coq 标准库中包含了一个不同的 ASCII 字符串的归纳定义。然而，为了应用
    之前定义的匹配关系，我们在此使用刚刚给出的 ASCII 字符列表作为定义。

<div class="paragraph"> </div>

    我们也可以定义工作在多态列表上的正则表达式匹配器，而非特定于 ASCII 字符列表。
    我们将要实现的匹配算法需要知道如何对列表中的元素判断相等，因此需要给定一个
    相等关系测试函数。一般化我们给出的定义、定理和证明有一点枯燥，但是可行的。 
<div class="paragraph"> </div>

 正则表达式匹配器的正确性证明会由匹配函数的性质和 <span class="inlinecode"><span class="id" type="keyword">match</span></span> 关系的性质组成，
    <span class="inlinecode"><span class="id" type="keyword">match</span></span> 关系并不依赖匹配函数。我们将会首先证明后一类性质。他们中的多数
    将会是很直接的证明，已经被直接给出；少部分关键的引理会留给你来证明。 
</div>

<div class="doc">
每个可被证明的 <span class="inlinecode"><span class="id" type="keyword">Prop</span></span> 等价于 <span class="inlinecode"><span class="id" type="var">True</span></span>。 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">provable_equiv_true</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> : <span class="id" type="keyword">Prop</span>), <span class="id" type="var">P</span> → (<span class="id" type="var">P</span> ↔ <span class="id" type="var">True</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">intros</span>. <span class="id" type="var">constructor</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">intros</span> <span class="id" type="var">_</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
其逆可被证明的 <span class="inlinecode"><span class="id" type="keyword">Prop</span></span> 等价于 <span class="inlinecode"><span class="id" type="var">False</span></span>。 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">not_equiv_false</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">P</span> : <span class="id" type="keyword">Prop</span>), ¬<span class="id" type="var">P</span> → (<span class="id" type="var">P</span> ↔ <span class="id" type="var">False</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">destruct</span> <span class="id" type="var">H<sub>0</sub></span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<span class="inlinecode"><span class="id" type="var">EmptySet</span></span> 不匹配字符串。 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">null_matches_none</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">s</span> : <span class="id" type="var">string</span>), (<span class="id" type="var">s</span> =~ <span class="id" type="var">EmptySet</span>) ↔ <span class="id" type="var">False</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">not_equiv_false</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">not</span>. <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<span class="inlinecode"><span class="id" type="var">EmptyStr</span></span> 仅匹配空字符串。 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">empty_matches_eps</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">s</span> : <span class="id" type="var">string</span>), <span class="id" type="var">s</span> =~ <span class="id" type="var">EmptyStr</span> ↔ <span class="id" type="var">s</span> = [ ].<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">MEmpty</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<span class="inlinecode"><span class="id" type="var">EmptyStr</span></span> 不匹配非空字符串。 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">empty_nomatch_ne</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">a</span> : <span class="id" type="var">ascii</span>) <span class="id" type="var">s</span>, (<span class="id" type="var">a</span> :: <span class="id" type="var">s</span> =~ <span class="id" type="var">EmptyStr</span>) ↔ <span class="id" type="var">False</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">not_equiv_false</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">not</span>. <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<span class="inlinecode"><span class="id" type="var">Char</span></span> <span class="inlinecode"><span class="id" type="var">a</span></span> 不匹配不以 <span class="inlinecode"><span class="id" type="var">a</span></span> 字符开始的字符串。 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">char_nomatch_char</span> :<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">a</span> <span class="id" type="var">b</span> : <span class="id" type="var">ascii</span>) <span class="id" type="var">s</span>, <span class="id" type="var">b</span> ≠ <span class="id" type="var">a</span> → (<span class="id" type="var">b</span> :: <span class="id" type="var">s</span> =~ <span class="id" type="var">Char</span> <span class="id" type="var">a</span> ↔ <span class="id" type="var">False</span>).<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">not_equiv_false</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">unfold</span> <span class="id" type="var">not</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">inversion</span> <span class="id" type="var">H<sub>0</sub></span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">reflexivity</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
如果 <span class="inlinecode"><span class="id" type="var">Char</span></span> <span class="inlinecode"><span class="id" type="var">a</span></span> 匹配一个非空字符串，那么这个字符串的尾（tail）为空。 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">char_eps_suffix</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">a</span> : <span class="id" type="var">ascii</span>) <span class="id" type="var">s</span>, <span class="id" type="var">a</span> :: <span class="id" type="var">s</span> =~ <span class="id" type="var">Char</span> <span class="id" type="var">a</span> ↔ <span class="id" type="var">s</span> = [ ].<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">rewrite</span> <span class="id" type="var">H</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">MChar</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<span class="inlinecode"><span class="id" type="var">App</span></span> <span class="inlinecode"><span class="id" type="var">re<sub>0</sub></span></span> <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span> 匹配字符串 <span class="inlinecode"><span class="id" type="var">s</span></span> 当且仅当 <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">s<sub>0</sub></span></span> <span class="inlinecode">++</span> <span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span></span>，其中 <span class="inlinecode"><span class="id" type="var">s<sub>0</sub></span></span>
    匹配 <span class="inlinecode"><span class="id" type="var">re<sub>0</sub></span></span> 且 <span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span></span> 匹配 <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span>。 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">app_exists</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">s</span> : <span class="id" type="var">string</span>) <span class="id" type="var">re<sub>0</sub></span> <span class="id" type="var">re<sub>1</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">s</span> =~ <span class="id" type="var">App</span> <span class="id" type="var">re<sub>0</sub></span> <span class="id" type="var">re<sub>1</sub></span> ↔<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">s<sub>0</sub></span> <span class="id" type="var">s<sub>1</sub></span>, <span class="id" type="var">s</span> = <span class="id" type="var">s<sub>0</sub></span> ++ <span class="id" type="var">s<sub>1</sub></span> ∧ <span class="id" type="var">s<sub>0</sub></span> =~ <span class="id" type="var">re<sub>0</sub></span> ∧ <span class="id" type="var">s<sub>1</sub></span> =~ <span class="id" type="var">re<sub>1</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">split</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>. <span style='font-size:120%;'>&exist;</span><span class="id" type="var">s<sub>1</sub></span>, <span class="id" type="var">s<sub>2</sub></span>. <span class="id" type="tactic">split</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;* <span class="id" type="tactic">reflexivity</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;* <span class="id" type="tactic">split</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>3</sub></span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>4</sub></span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">intros</span> [ <span class="id" type="var">s<sub>0</sub></span> [ <span class="id" type="var">s<sub>1</sub></span> [ <span class="id" type="var">Happ</span> [ <span class="id" type="var">Hmat0</span> <span class="id" type="var">Hmat1</span> ] ] ] ].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="tactic">rewrite</span> <span class="id" type="var">Happ</span>. <span class="id" type="tactic">apply</span> (<span class="id" type="var">MApp</span> <span class="id" type="var">s<sub>0</sub></span> <span class="id" type="var">_</span> <span class="id" type="var">s<sub>1</sub></span> <span class="id" type="var">_</span> <span class="id" type="var">Hmat0</span> <span class="id" type="var">Hmat1</span>).<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab246"></a><h4 class="section">练习：3 星, standard, optional (app_ne)</h4>
 <span class="inlinecode"><span class="id" type="var">App</span></span> <span class="inlinecode"><span class="id" type="var">re<sub>0</sub></span></span> <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span> 匹配 <span class="inlinecode"><span class="id" type="var">a</span>::<span class="id" type="var">s</span></span> 当且仅当 <span class="inlinecode"><span class="id" type="var">re<sub>0</sub></span></span> 匹配空字符串
    且 <span class="inlinecode"><span class="id" type="var">a</span>::<span class="id" type="var">s</span></span> 匹配 <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span> 或 <span class="inlinecode"><span class="id" type="var">s</span>=<span class="id" type="var">s<sub>0</sub></span>++<span class="id" type="var">s<sub>1</sub></span></span>，其中 <span class="inlinecode"><span class="id" type="var">a</span>::<span class="id" type="var">s<sub>0</sub></span></span> 匹配 <span class="inlinecode"><span class="id" type="var">re<sub>0</sub></span></span>
    且 <span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span></span> 匹配 <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span>。

<div class="paragraph"> </div>

    尽管这个性质由纯粹的匹配关系构成，它是隐藏在匹配器的设计背后的一个重要观察。
    因此（1）花一些时间理解它，（2）证明它，并且（3）留心后面你会如何使用它。
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">app_ne</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">a</span> : <span class="id" type="var">ascii</span>) <span class="id" type="var">s</span> <span class="id" type="var">re<sub>0</sub></span> <span class="id" type="var">re<sub>1</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">a</span> :: <span class="id" type="var">s</span> =~ (<span class="id" type="var">App</span> <span class="id" type="var">re<sub>0</sub></span> <span class="id" type="var">re<sub>1</sub></span>) ↔<br/>
&nbsp;&nbsp;&nbsp;&nbsp;([ ] =~ <span class="id" type="var">re<sub>0</sub></span> ∧ <span class="id" type="var">a</span> :: <span class="id" type="var">s</span> =~ <span class="id" type="var">re<sub>1</sub></span>) ∨<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">s<sub>0</sub></span> <span class="id" type="var">s<sub>1</sub></span>, <span class="id" type="var">s</span> = <span class="id" type="var">s<sub>0</sub></span> ++ <span class="id" type="var">s<sub>1</sub></span> ∧ <span class="id" type="var">a</span> :: <span class="id" type="var">s<sub>0</sub></span> =~ <span class="id" type="var">re<sub>0</sub></span> ∧ <span class="id" type="var">s<sub>1</sub></span> =~ <span class="id" type="var">re<sub>1</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 <span class="inlinecode"><span class="id" type="var">s</span></span> 匹配 <span class="inlinecode"><span class="id" type="var">Union</span></span> <span class="inlinecode"><span class="id" type="var">re<sub>0</sub></span></span> <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span> 当且仅当 <span class="inlinecode"><span class="id" type="var">s</span></span> 匹配 <span class="inlinecode"><span class="id" type="var">re<sub>0</sub></span></span> 或 <span class="inlinecode"><span class="id" type="var">s</span></span> 匹配 <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span>. 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">union_disj</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">s</span> : <span class="id" type="var">string</span>) <span class="id" type="var">re<sub>0</sub></span> <span class="id" type="var">re<sub>1</sub></span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">s</span> =~ <span class="id" type="var">Union</span> <span class="id" type="var">re<sub>0</sub></span> <span class="id" type="var">re<sub>1</sub></span> ↔ <span class="id" type="var">s</span> =~ <span class="id" type="var">re<sub>0</sub></span> ∨ <span class="id" type="var">s</span> =~ <span class="id" type="var">re<sub>1</sub></span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="id" type="tactic">intros</span>. <span class="id" type="tactic">split</span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">intros</span>. <span class="id" type="tactic">inversion</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="var">left</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>2</sub></span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="var">right</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H<sub>1</sub></span>.<br/>
&nbsp;&nbsp;- <span class="id" type="tactic">intros</span> [ <span class="id" type="var">H</span> | <span class="id" type="var">H</span> ].<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="tactic">apply</span> <span class="id" type="var">MUnionL</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
&nbsp;&nbsp;&nbsp;&nbsp;+ <span class="id" type="tactic">apply</span> <span class="id" type="var">MUnionR</span>. <span class="id" type="tactic">apply</span> <span class="id" type="var">H</span>.<br/>
<span class="id" type="keyword">Qed</span>.<br/>
</div>

<div class="doc">
<a name="lab247"></a><h4 class="section">练习：3 星, standard, optional (star_ne)</h4>
 <span class="inlinecode"><span class="id" type="var">a</span>::<span class="id" type="var">s</span></span> 匹配 <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span> 当且仅当 <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=</span> <span class="inlinecode"><span class="id" type="var">s<sub>0</sub></span></span> <span class="inlinecode">++</span> <span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span></span>，其中 <span class="inlinecode"><span class="id" type="var">a</span>::<span class="id" type="var">s<sub>0</sub></span></span> 匹配
    <span class="inlinecode"><span class="id" type="var">re</span></span> 且 <span class="inlinecode"><span class="id" type="var">s<sub>1</sub></span></span> 匹配 <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span>。 同 <span class="inlinecode"><span class="id" type="var">app_ne</span></span>一样，这个观察很重要，
    因此理解，证明并留意它。

<div class="paragraph"> </div>

    提示：你需要进行归纳。的确是有几个合理的候选 <span class="inlinecode"><span class="id" type="keyword">Prop</span></span> 来进行归纳。
    但唯一其作用的方式是首先拆分 <span class="inlinecode"><span class="id" type="var">iff</span></span> 为两个蕴含式，然后在 <span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode">::</span> <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=~</span> <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span>
    的证据上进行归纳来证明其中一个。另一个蕴含式可以无需使用归纳来证明。

<div class="paragraph"> </div>

    为了在正确的性质上归纳，你需要使用 <span class="inlinecode"><span class="id" type="var">remember</span></span> 策略来重新表述 <span class="inlinecode"><span class="id" type="var">a</span></span> <span class="inlinecode">::</span> <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=~</span> <span class="inlinecode"><span class="id" type="var">Star</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span>，
    使其成为一般变量上的 <span class="inlinecode"><span class="id" type="keyword">Prop</span></span>。 
</div>
<div class="code code-tight">

<span class="id" type="keyword">Lemma</span> <span class="id" type="var">star_ne</span> : <span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">a</span> : <span class="id" type="var">ascii</span>) <span class="id" type="var">s</span> <span class="id" type="var">re</span>,<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span class="id" type="var">a</span> :: <span class="id" type="var">s</span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span> ↔<br/>
&nbsp;&nbsp;&nbsp;&nbsp;<span style='font-size:120%;'>&exist;</span><span class="id" type="var">s<sub>0</sub></span> <span class="id" type="var">s<sub>1</sub></span>, <span class="id" type="var">s</span> = <span class="id" type="var">s<sub>0</sub></span> ++ <span class="id" type="var">s<sub>1</sub></span> ∧ <span class="id" type="var">a</span> :: <span class="id" type="var">s<sub>0</sub></span> =~ <span class="id" type="var">re</span> ∧ <span class="id" type="var">s<sub>1</sub></span> =~ <span class="id" type="var">Star</span> <span class="id" type="var">re</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 我们的正则表达式匹配器定义包括两个不动点函数。第一个函数对给定的正则表达式 <span class="inlinecode"><span class="id" type="var">re</span></span>
    进行求值，结果映射了 <span class="inlinecode"><span class="id" type="var">re</span></span> 是否匹配空字符串。这个函数满足以下性质： 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Definition</span> <span class="id" type="var">refl_matches_eps</span> <span class="id" type="var">m</span> :=<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">re</span> : @<span class="id" type="var">reg_exp</span> <span class="id" type="var">ascii</span>, <span class="id" type="var">reflect</span> ([ ] =~ <span class="id" type="var">re</span>) (<span class="id" type="var">m</span> <span class="id" type="var">re</span>).<br/>
</div>

<div class="doc">
<a name="lab248"></a><h4 class="section">练习：2 星, standard, optional (match_eps)</h4>
 完成 <span class="inlinecode"><span class="id" type="var">match_eps</span></span> 的定义，其测试给定的正则表达式是否匹配空字符串： 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">match_eps</span> (<span class="id" type="var">re</span>: @<span class="id" type="var">reg_exp</span> <span class="id" type="var">ascii</span>) : <span class="id" type="var">bool</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab249"></a><h4 class="section">练习：3 星, standard, optional (match_eps_refl)</h4>
 现在，请证明 <span class="inlinecode"><span class="id" type="var">match_eps</span></span> 确实测试了给定的正则表达式是否匹配空字符串。
    （提示：你会使用到互映引理 <span class="inlinecode"><span class="id" type="var">ReflectT</span></span> 和 <span class="inlinecode"><span class="id" type="var">ReflectF</span></span>。） 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">match_eps_refl</span> : <span class="id" type="var">refl_matches_eps</span> <span class="id" type="var">match_eps</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 我们将会定义其他函数也使用到 <span class="inlinecode"><span class="id" type="var">match_eps</span></span>。然而，这些函数的证明中你唯一会用到的
    <span class="inlinecode"><span class="id" type="var">match_eps</span></span> 的性质是 <span class="inlinecode"><span class="id" type="var">match_eps_refl</span></span>。
</div>

<div class="doc">
我们匹配器所进行的关键操作是迭代地构造一个正则表达式生成式的序列。
    对于字符 <span class="inlinecode"><span class="id" type="var">a</span></span> 和正则表达式 <span class="inlinecode"><span class="id" type="var">re</span></span>，<span class="inlinecode"><span class="id" type="var">re</span></span> 在 <span class="inlinecode"><span class="id" type="var">a</span></span> 上的生成式是一个正则表达式，
    其匹配所有匹配 <span class="inlinecode"><span class="id" type="var">re</span></span> 且以 <span class="inlinecode"><span class="id" type="var">a</span></span> 开始的字符串的后缀。也即，<span class="inlinecode"><span class="id" type="var">re'</span></span>
    是 <span class="inlinecode"><span class="id" type="var">re</span></span> 在 <span class="inlinecode"><span class="id" type="var">a</span></span> 上的一个生成式如果他们满足以下关系：
</div>
<div class="code code-tight">

<span class="id" type="keyword">Definition</span> <span class="id" type="var">is_der</span> <span class="id" type="var">re</span> (<span class="id" type="var">a</span> : <span class="id" type="var">ascii</span>) <span class="id" type="var">re'</span> :=<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span><span class="id" type="var">s</span>, <span class="id" type="var">a</span> :: <span class="id" type="var">s</span> =~ <span class="id" type="var">re</span> ↔ <span class="id" type="var">s</span> =~ <span class="id" type="var">re'</span>.<br/>
</div>

<div class="doc">
函数 <span class="inlinecode"><span class="id" type="var">d</span></span> 生成字符串如果对于给定的字符 <span class="inlinecode"><span class="id" type="var">a</span></span> 和正则表达式 <span class="inlinecode"><span class="id" type="var">re</span></span>，
    它求值为 <span class="inlinecode"><span class="id" type="var">re</span></span> 在 <span class="inlinecode"><span class="id" type="var">a</span></span> 上的生成式。也即，<span class="inlinecode"><span class="id" type="var">d</span></span> 满足以下关系： 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Definition</span> <span class="id" type="var">derives</span> <span class="id" type="var">d</span> := <span style='font-size:120%;'>&forall;</span><span class="id" type="var">a</span> <span class="id" type="var">re</span>, <span class="id" type="var">is_der</span> <span class="id" type="var">re</span> <span class="id" type="var">a</span> (<span class="id" type="var">d</span> <span class="id" type="var">a</span> <span class="id" type="var">re</span>).<br/>
</div>

<div class="doc">
<a name="lab250"></a><h4 class="section">练习：3 星, standard, optional (derive)</h4>
 请定义 <span class="inlinecode"><span class="id" type="var">derive</span></span> 使其生成字符串。一个自然的实现是在某些分类使用
    <span class="inlinecode"><span class="id" type="var">match_eps</span></span> 来判断正则表达式是否匹配空字符串。 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">derive</span> (<span class="id" type="var">a</span> : <span class="id" type="var">ascii</span>) (<span class="id" type="var">re</span> : @<span class="id" type="var">reg_exp</span> <span class="id" type="var">ascii</span>) : @<span class="id" type="var">reg_exp</span> <span class="id" type="var">ascii</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 <span class="inlinecode"><span class="id" type="var">derive</span></span> 函数应当通过以下测试。每个测试都在将被匹配器所求值的表达式和
    最终被匹配器返回的结果之间确立一种相等关系。
    每个测试也被添加了它所反映的匹配事实的注解。
</div>
<div class="code code-tight">
<span class="id" type="keyword">Example</span> <span class="id" type="var">c</span> := <span class="id" type="var">ascii_of_nat</span> 99.<br/>
<span class="id" type="keyword">Example</span> <span class="id" type="var">d</span> := <span class="id" type="var">ascii_of_nat</span> 100.<br/>
</div>

<div class="doc">
"c" =~ EmptySet: 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_der0</span> : <span class="id" type="var">match_eps</span> (<span class="id" type="var">derive</span> <span class="id" type="var">c</span> (<span class="id" type="var">EmptySet</span>)) = <span class="id" type="var">false</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
"c" =~ Char c: 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_der1</span> : <span class="id" type="var">match_eps</span> (<span class="id" type="var">derive</span> <span class="id" type="var">c</span> (<span class="id" type="var">Char</span> <span class="id" type="var">c</span>)) = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
"c" =~ Char d: 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_der2</span> : <span class="id" type="var">match_eps</span> (<span class="id" type="var">derive</span> <span class="id" type="var">c</span> (<span class="id" type="var">Char</span> <span class="id" type="var">d</span>)) = <span class="id" type="var">false</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
"c" =~ App (Char c) EmptyStr: 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_der3</span> : <span class="id" type="var">match_eps</span> (<span class="id" type="var">derive</span> <span class="id" type="var">c</span> (<span class="id" type="var">App</span> (<span class="id" type="var">Char</span> <span class="id" type="var">c</span>) <span class="id" type="var">EmptyStr</span>)) = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
"c" =~ App EmptyStr (Char c): 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_der4</span> : <span class="id" type="var">match_eps</span> (<span class="id" type="var">derive</span> <span class="id" type="var">c</span> (<span class="id" type="var">App</span> <span class="id" type="var">EmptyStr</span> (<span class="id" type="var">Char</span> <span class="id" type="var">c</span>))) = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
"c" =~ Star c: 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_der5</span> : <span class="id" type="var">match_eps</span> (<span class="id" type="var">derive</span> <span class="id" type="var">c</span> (<span class="id" type="var">Star</span> (<span class="id" type="var">Char</span> <span class="id" type="var">c</span>))) = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
"cd" =~ App (Char c) (Char d): 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_der6</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">match_eps</span> (<span class="id" type="var">derive</span> <span class="id" type="var">d</span> (<span class="id" type="var">derive</span> <span class="id" type="var">c</span> (<span class="id" type="var">App</span> (<span class="id" type="var">Char</span> <span class="id" type="var">c</span>) (<span class="id" type="var">Char</span> <span class="id" type="var">d</span>)))) = <span class="id" type="var">true</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
"cd" =~ App (Char d) (Char c): 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Example</span> <span class="id" type="var">test_der7</span> :<br/>
&nbsp;&nbsp;<span class="id" type="var">match_eps</span> (<span class="id" type="var">derive</span> <span class="id" type="var">d</span> (<span class="id" type="var">derive</span> <span class="id" type="var">c</span> (<span class="id" type="var">App</span> (<span class="id" type="var">Char</span> <span class="id" type="var">d</span>) (<span class="id" type="var">Char</span> <span class="id" type="var">c</span>)))) = <span class="id" type="var">false</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<div class="doc">
<a name="lab251"></a><h4 class="section">练习：4 星, standard, optional (derive_corr)</h4>
 请证明 <span class="inlinecode"><span class="id" type="var">derive</span></span> 确实总是会生成字符串。

<div class="paragraph"> </div>

    提示：一种证明方法是对 <span class="inlinecode"><span class="id" type="var">re</span></span> 归纳，尽管你需要通过归纳和一般化合适的项来
    仔细选择要证明的性质。

<div class="paragraph"> </div>

    提示：如果你定义的 <span class="inlinecode"><span class="id" type="var">derive</span></span> 对某个正则表达式 <span class="inlinecode"><span class="id" type="var">re</span></span> 使用了 <span class="inlinecode"><span class="id" type="var">match_eps</span></span>，
    那么可对 <span class="inlinecode"><span class="id" type="var">re</span></span> 应用 <span class="inlinecode"><span class="id" type="var">match_eps_refl</span></span>，接着对结果解构并生成
    分类，其中你可以假设 <span class="inlinecode"><span class="id" type="var">re</span></span> 匹配或不匹配空字符串。

<div class="paragraph"> </div>

    提示：通过使用之前证明过的引理可以帮助一点你的工作。特别是，在证明归纳的
    许多分类时，通过之前的引理，你可以用一个复杂的正则表达式（比如，
    <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=~</span> <span class="inlinecode"><span class="id" type="var">Union</span></span> <span class="inlinecode"><span class="id" type="var">re<sub>0</sub></span></span> <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span>）来重写命题，得到一个简单正则表达式上的命
    题构成的布尔表达式（比如，<span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=~</span> <span class="inlinecode"><span class="id" type="var">re<sub>0</sub></span></span> <span class="inlinecode">∨</span> <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=~</span> <span class="inlinecode"><span class="id" type="var">re<sub>1</sub></span></span>）。
    你可以使用 <span class="inlinecode"><span class="id" type="tactic">intro</span></span> 和 <span class="inlinecode"><span class="id" type="tactic">destruct</span></span> 来对这些命题进行推理。
</div>
<div class="code code-tight">
<span class="id" type="keyword">Lemma</span> <span class="id" type="var">derive_corr</span> : <span class="id" type="var">derives</span> <span class="id" type="var">derive</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

 我们将会使用 <span class="inlinecode"><span class="id" type="var">derive</span></span> 来定义正则表达式匹配器。然而，在匹配器的性质的证明中你唯一会用到
    的 <span class="inlinecode"><span class="id" type="var">derive</span></span> 的性质是 <span class="inlinecode"><span class="id" type="var">derive_corr</span></span>。 
</div>

<div class="doc">
函数 <span class="inlinecode"><span class="id" type="var">m</span></span> 匹配正则表达式如果对给定的字符串 <span class="inlinecode"><span class="id" type="var">s</span></span> 和正则表达式 <span class="inlinecode"><span class="id" type="var">re</span></span>，
    它求值的结果映射了 <span class="inlinecode"><span class="id" type="var">s</span></span> 是否被 <span class="inlinecode"><span class="id" type="var">re</span></span> 匹配。也即，<span class="inlinecode"><span class="id" type="var">m</span></span> 满足以下性质：
</div>
<div class="code code-tight">
<span class="id" type="keyword">Definition</span> <span class="id" type="var">matches_regex</span> <span class="id" type="var">m</span> : <span class="id" type="keyword">Prop</span> :=<br/>
&nbsp;&nbsp;<span style='font-size:120%;'>&forall;</span>(<span class="id" type="var">s</span> : <span class="id" type="var">string</span>) <span class="id" type="var">re</span>, <span class="id" type="var">reflect</span> (<span class="id" type="var">s</span> =~ <span class="id" type="var">re</span>) (<span class="id" type="var">m</span> <span class="id" type="var">s</span> <span class="id" type="var">re</span>).<br/>
</div>

<div class="doc">
<a name="lab252"></a><h4 class="section">练习：2 星, standard, optional (regex_match)</h4>
 完成 <span class="inlinecode"><span class="id" type="var">regex_match</span></span> 的定义，使其可以匹配正则表达式。
</div>
<div class="code code-tight">
<span class="id" type="keyword">Fixpoint</span> <span class="id" type="var">regex_match</span> (<span class="id" type="var">s</span> : <span class="id" type="var">string</span>) (<span class="id" type="var">re</span> : @<span class="id" type="var">reg_exp</span> <span class="id" type="var">ascii</span>) : <span class="id" type="var">bool</span><br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;将本行替换成&nbsp;":=&nbsp;_你的_定义_&nbsp;."&nbsp;*)</span>. <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="doc less-space">
<div class="paragraph"> </div>

<a name="lab253"></a><h4 class="section">练习：3 星, standard, optional (regex_refl)</h4>
 最后，证明 <span class="inlinecode"><span class="id" type="var">regex_match</span></span> 确实可以匹配正则表达式。

<div class="paragraph"> </div>

    提示：如果你定义的 <span class="inlinecode"><span class="id" type="var">regex_match</span></span> 对正则表达式 <span class="inlinecode"><span class="id" type="var">re</span></span> 使用了 <span class="inlinecode"><span class="id" type="var">match_eps</span></span>，
    那么可对 <span class="inlinecode"><span class="id" type="var">re</span></span> 应用 <span class="inlinecode"><span class="id" type="var">match_eps_refl</span></span>，接着对结果解构并生成
    分类，其中你可以假设 <span class="inlinecode"><span class="id" type="var">re</span></span> 匹配或不匹配空字符串。

<div class="paragraph"> </div>

    提示：如果你定义的 <span class="inlinecode"><span class="id" type="var">regex_match</span></span> 对字符 <span class="inlinecode"><span class="id" type="var">x</span></span> 和正则表达式 <span class="inlinecode"><span class="id" type="var">re</span></span> 使用了 <span class="inlinecode"><span class="id" type="var">derive</span></span>，
    那么可对 <span class="inlinecode"><span class="id" type="var">x</span></span> 和 <span class="inlinecode"><span class="id" type="var">re</span></span> 应用 <span class="inlinecode"><span class="id" type="var">derive_corr</span></span>，以此证明 <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode">::</span> <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=~</span> <span class="inlinecode"><span class="id" type="var">re</span></span> 当给定
    <span class="inlinecode"><span class="id" type="var">s</span></span> <span class="inlinecode">=~</span> <span class="inlinecode"><span class="id" type="var">derive</span></span> <span class="inlinecode"><span class="id" type="var">x</span></span> <span class="inlinecode"><span class="id" type="var">re</span></span> 时，反之亦然。 
</div>
<div class="code code-tight">
<span class="id" type="keyword">Theorem</span> <span class="id" type="var">regex_refl</span> : <span class="id" type="var">matches_regex</span> <span class="id" type="var">regex_match</span>.<br/>
<span class="id" type="keyword">Proof</span>.<br/>
&nbsp;&nbsp;<span class="comment">(*&nbsp;请在此处解答&nbsp;*)</span> <span class="id" type="var">Admitted</span>.<br/>
</div>

<span class="proofbox">&#9744;</span> 
<div class="code code-tight">

<span class="comment">(*&nbsp;Mon&nbsp;Oct&nbsp;28&nbsp;08:14:24&nbsp;UTC&nbsp;2019&nbsp;*)</span><br/>
</div>
</div>



</div>

</body>
</html>